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 mvrladdi.1 B
mvrladdi.2 C
mvrladdi.3 A = B + C
Assertion mvrladdi A B = C

Proof

Step Hyp Ref Expression
1 mvrladdi.1 B
2 mvrladdi.2 C
3 mvrladdi.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