Theorem mvrraddd

Description: Move the right 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	mvrraddd	$$⊢\phi \to A-C=B$$

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	3	oveq1d	$$⊢\phi \to A-C=B+C-C$$
5	1 2	pncand	$$⊢\phi \to B+C-C=B$$
6	4 5	eqtrd	$$⊢\phi \to A-C=B$$