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	|- ( ph -> B e. CC )
	rsubrotld.c	|- ( ph -> C e. CC )
	rsubrotld.1	|- ( ph -> A = ( B - C ) )
Assertion	rsubrotld	|- ( ph -> B = ( C + A ) )

Proof

Step	Hyp	Ref	Expression
1		rsubrotld.b	|- ( ph -> B e. CC )
2		rsubrotld.c	|- ( ph -> C e. CC )
3		rsubrotld.1	|- ( ph -> A = ( B - C ) )
4	3	eqcomd	|- ( ph -> ( B - C ) = A )
5	1 2 4	lsubrotld	|- ( ph -> ( C + A ) = B )
6	5	eqcomd	|- ( ph -> B = ( C + A ) )