Theorem lsubrotld

Description: Rotate the variables left in an equation with subtraction on the left, converting it into an addition. (Contributed by SN, 21-Aug-2024)

	Ref	Expression
Hypotheses	lsubrotld.a	|- ( ph -> A e. CC )
	lsubrotld.b	|- ( ph -> B e. CC )
	lsubrotld.1	|- ( ph -> ( A - B ) = C )
Assertion	lsubrotld	|- ( ph -> ( B + C ) = A )

Proof

Step	Hyp	Ref	Expression
1		lsubrotld.a	|- ( ph -> A e. CC )
2		lsubrotld.b	|- ( ph -> B e. CC )
3		lsubrotld.1	|- ( ph -> ( A - B ) = C )
4	1 2	subcld	|- ( ph -> ( A - B ) e. CC )
5	3 4	eqeltrrd	|- ( ph -> C e. CC )
6	2 5	addcld	|- ( ph -> ( B + C ) e. CC )
7	2 5	pncan2d	|- ( ph -> ( ( B + C ) - B ) = C )
8	7 3	eqtr4d	|- ( ph -> ( ( B + C ) - B ) = ( A - B ) )
9	6 1 2 8	subcan2d	|- ( ph -> ( B + C ) = A )