Metamath Proof Explorer


Theorem mvrrsubd

Description: Move a subtraction in the RHS to a right-addition in the LHS. Converse of mvlraddd . (Contributed by SN, 21-Aug-2024)

Ref Expression
Hypotheses mvrrsubd.a φ B
mvrrsubd.b φ C
mvrrsubd.1 φ A = B C
Assertion mvrrsubd φ A + C = B

Proof

Step Hyp Ref Expression
1 mvrrsubd.a φ B
2 mvrrsubd.b φ C
3 mvrrsubd.1 φ A = B C
4 1 2 subcld φ B C
5 3 4 eqeltrd φ A
6 5 2 addcld φ A + C
7 5 2 pncand φ A + C - C = A
8 7 3 eqtrd φ A + C - C = B C
9 6 1 2 8 subcan2d φ A + C = B