Theorem mvrraddi

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

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

Proof

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