Theorem raddcom12d

Description: Swap the first two variables in an equation with addition on the right, converting it into a subtraction. Version of mvrraddd with a commuted consequent, and of mvlraddd with a commuted hypothesis. (Contributed by SN, 21-Aug-2024)

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

Proof

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