Theorem rsubrotld

Description: Rotate the variables left in an equation with subtraction on the right, converting it into an addition.

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

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

Proof

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