Theorem mvlraddi

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

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

Proof

Step	Hyp	Ref	Expression
1		mvlraddi.1	$$⊢A\in ℂ$$
2		mvlraddi.2	$$⊢B\in ℂ$$
3		mvlraddi.3	$$⊢A+B=C$$
4	1 2	pncan3oi	$$⊢A+B-B=A$$
5	3	oveq1i	$$⊢A+B-B=C-B$$
6	4 5	eqtr3i	$$⊢A=C-B$$