Theorem lsubrotld

Description: Rotate the variables left in an equation with subtraction on the left, 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, 21-Aug-2024)

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

Proof

Step	Hyp	Ref	Expression
1		lsubrotld.a	$$⊢\phi \to A\in ℂ$$
2		lsubrotld.b	$$⊢\phi \to B\in ℂ$$
3		lsubrotld.1	$$⊢\phi \to A-B=C$$
4	1 2	subcld	$$⊢\phi \to A-B\in ℂ$$
5	3 4	eqeltrrd	$$⊢\phi \to C\in ℂ$$
6	2 5	addcld	$$⊢\phi \to B+C\in ℂ$$
7	2 5	pncan2d	$$⊢\phi \to B+C-B=C$$
8	7 3	eqtr4d	$$⊢\phi \to B+C-B=A-B$$
9	6 1 2 8	subcan2d	$$⊢\phi \to B+C=A$$