Theorem mvrladdd

Description: Move the left term in a sum on the RHS to the LHS, deduction form. (Contributed by David A. Wheeler, 11-Oct-2018)

	Ref	Expression
Hypotheses	mvrraddd.1	$$⊢\phi \to B\in ℂ$$
	mvrraddd.2	$$⊢\phi \to C\in ℂ$$
	mvrraddd.3	$$⊢\phi \to A=B+C$$
Assertion	mvrladdd	$$⊢\phi \to A-B=C$$

Proof

Step	Hyp	Ref	Expression
1		mvrraddd.1	$$⊢\phi \to B\in ℂ$$
2		mvrraddd.2	$$⊢\phi \to C\in ℂ$$
3		mvrraddd.3	$$⊢\phi \to A=B+C$$
4	1 2 3	comraddd	$$⊢\phi \to A=C+B$$
5	2 1 4	mvrraddd	$$⊢\phi \to A-B=C$$