Theorem laddrotrd

Description: Rotate the variables right in an equation with addition on the left, converting it into a subtraction. Version of mvlladdd with a commuted consequent, and of mvrladdd with a commuted hypothesis. (Contributed by SN, 21-Aug-2024)

	Ref	Expression
Hypotheses	laddrotrd.a	⊢ ( 𝜑 → 𝐴 ∈ ℂ )
	laddrotrd.b	⊢ ( 𝜑 → 𝐵 ∈ ℂ )
	laddrotrd.1	⊢ ( 𝜑 → ( 𝐴 + 𝐵 ) = 𝐶 )
Assertion	laddrotrd	⊢ ( 𝜑 → ( 𝐶 − 𝐴 ) = 𝐵 )

Proof

Step	Hyp	Ref	Expression
1		laddrotrd.a	⊢ ( 𝜑 → 𝐴 ∈ ℂ )
2		laddrotrd.b	⊢ ( 𝜑 → 𝐵 ∈ ℂ )
3		laddrotrd.1	⊢ ( 𝜑 → ( 𝐴 + 𝐵 ) = 𝐶 )
4	1 2 3	mvlladdd	⊢ ( 𝜑 → 𝐵 = ( 𝐶 − 𝐴 ) )
5	4	eqcomd	⊢ ( 𝜑 → ( 𝐶 − 𝐴 ) = 𝐵 )