Theorem laddrotrd

Description: Rotate the variables right in an equation with addition on the left, converting it into a subtraction. Version of mvlladdd with a commuted consequent, and of mvrladdd with a commuted hypothesis. (Contributed by SN, 21-Aug-2024)

	Ref	Expression
Hypotheses	laddrotrd.a	$$⊢\phi \to A\in ℂ$$
	laddrotrd.b	$$⊢\phi \to B\in ℂ$$
	laddrotrd.1	$$⊢\phi \to A+B=C$$
Assertion	laddrotrd	$$⊢\phi \to C-A=B$$

Proof

Step	Hyp	Ref	Expression
1		laddrotrd.a	$$⊢\phi \to A\in ℂ$$
2		laddrotrd.b	$$⊢\phi \to B\in ℂ$$
3		laddrotrd.1	$$⊢\phi \to A+B=C$$
4	1 2 3	mvlladdd	$$⊢\phi \to B=C-A$$
5	4	eqcomd	$$⊢\phi \to C-A=B$$