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