This paper introduces a novel axiomatic proof calculus for differential-algebraic dynamic logic (dAL). The calculus enables deductive verification and sound transformation of differential-algebraic programs (DAPs), which generalize differential-algebraic equations, while remaining compatible with differential dynamic logic (dL) for hybrid programs. One central contribution is the ghost switching axiom which establishes precise conditions to decompose multi-modal DAPs into equivalent hybrid systems with ordinary differential equations. The applicability of the calculus is demonstrated through a formal equivalence proof, showing the reduction of the Euclidean pendulum from a differential-algebraic formulation to an equivalent system of ordinary differential equations.