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	⊢ ( 𝜑 → 𝐵 ∈ ℂ )
	rsubrotld.c	⊢ ( 𝜑 → 𝐶 ∈ ℂ )
	rsubrotld.1	⊢ ( 𝜑 → 𝐴 = ( 𝐵 − 𝐶 ) )
Assertion	rsubrotld	⊢ ( 𝜑 → 𝐵 = ( 𝐶 + 𝐴 ) )

Proof

Step	Hyp	Ref	Expression
1		rsubrotld.b	⊢ ( 𝜑 → 𝐵 ∈ ℂ )
2		rsubrotld.c	⊢ ( 𝜑 → 𝐶 ∈ ℂ )
3		rsubrotld.1	⊢ ( 𝜑 → 𝐴 = ( 𝐵 − 𝐶 ) )
4	3	eqcomd	⊢ ( 𝜑 → ( 𝐵 − 𝐶 ) = 𝐴 )
5	1 2 4	lsubrotld	⊢ ( 𝜑 → ( 𝐶 + 𝐴 ) = 𝐵 )
6	5	eqcomd	⊢ ( 𝜑 → 𝐵 = ( 𝐶 + 𝐴 ) )