Theorem mvlraddd

Description: Move LHS right addition to RHS. (Contributed by David A. Wheeler, 15-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$$