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	⊢ 𝐴 ∈ ℂ
	mvlraddi.2	⊢ 𝐵 ∈ ℂ
	mvlraddi.3	⊢ ( 𝐴 + 𝐵 ) = 𝐶
Assertion	mvlraddi	⊢ 𝐴 = ( 𝐶 − 𝐵 )

Proof

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