Theorem mvrladdi

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

	Ref	Expression
Hypotheses	mvrladdi.1	⊢ 𝐵 ∈ ℂ
	mvrladdi.2	⊢ 𝐶 ∈ ℂ
	mvrladdi.3	⊢ 𝐴 = ( 𝐵 + 𝐶 )
Assertion	mvrladdi	⊢ ( 𝐴 − 𝐵 ) = 𝐶

Proof

Step	Hyp	Ref	Expression
1		mvrladdi.1	⊢ 𝐵 ∈ ℂ
2		mvrladdi.2	⊢ 𝐶 ∈ ℂ
3		mvrladdi.3	⊢ 𝐴 = ( 𝐵 + 𝐶 )
4	1 2 3	comraddi	⊢ 𝐴 = ( 𝐶 + 𝐵 )
5	4	oveq1i	⊢ ( 𝐴 − 𝐵 ) = ( ( 𝐶 + 𝐵 ) − 𝐵 )
6	2 1	pncan3oi	⊢ ( ( 𝐶 + 𝐵 ) − 𝐵 ) = 𝐶
7	5 6	eqtri	⊢ ( 𝐴 − 𝐵 ) = 𝐶