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

Proof

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