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 ⊢ A ∈ ℂ
mvlladdi.2 ⊢ B ∈ ℂ
mvlladdi.3 ⊢ A + B = C
Assertion mvlladdi ⊢ B = C − A

Proof

Step Hyp Ref Expression
1 mvlladdi.1 ⊢ A ∈ ℂ
2 mvlladdi.2 ⊢ B ∈ ℂ
3 mvlladdi.3 ⊢ A + B = C
4 2 1 pncan3oi ⊢ B + A - A = B
5 1 2 3 addcomli ⊢ B + A = C
6 5 oveq1i ⊢ B + A - A = C − A
7 4 6 eqtr3i ⊢ B = C − A