Metamath Proof Explorer


Theorem mvlraddd

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

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

Proof

Step Hyp Ref Expression
1 mvlraddd.1 φ A
2 mvlraddd.2 φ B
3 mvlraddd.3 φ A + B = C
4 1 2 pncand φ A + B - B = A
5 3 oveq1d φ A + B - B = C B
6 4 5 eqtr3d φ A = C B