Theorem mvlraddd

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

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

Proof

Step	Hyp	Ref	Expression
1		mvlraddd.1	$$⊢\phi \to A\in ℂ$$
2		mvlraddd.2	$$⊢\phi \to B\in ℂ$$
3		mvlraddd.3	$$⊢\phi \to A+B=C$$
4	1 2	pncand	$$⊢\phi \to A+B-B=A$$
5	3	oveq1d	$$⊢\phi \to A+B-B=C-B$$
6	4 5	eqtr3d	$$⊢\phi \to A=C-B$$