Theorem raddswap12d

Description: Swap the first two variables in an equation with addition on the right, converting it into a subtraction. Version of mvrraddd with a commuted consequent, and of mvlraddd with a commuted hypothesis.

EDITORIAL: The label for this theorem is questionable. Do not move until it would have 7 uses: current additional uses: (none). (Contributed by SN, 21-Aug-2024)

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

Proof

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