Metamath Proof Explorer


Theorem mvlraddi

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

Ref Expression
Hypotheses mvlraddi.1 A
mvlraddi.2 B
mvlraddi.3 A + B = C
Assertion mvlraddi A = C B

Proof

Step Hyp Ref Expression
1 mvlraddi.1 A
2 mvlraddi.2 B
3 mvlraddi.3 A + B = C
4 1 2 pncan3oi A + B - B = A
5 3 oveq1i A + B - B = C B
6 4 5 eqtr3i A = C B