This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem mvlladdi

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

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

Proof

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