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

Metamath Proof Explorer

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

Proof

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