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 | ||
mvrrsubd.b | |||
mvrrsubd.1 | |||
Assertion | mvrrsubd |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | mvrrsubd.a | ||
2 | mvrrsubd.b | ||
3 | mvrrsubd.1 | ||
4 | 1 2 | subcld | |
5 | 3 4 | eqeltrd | |
6 | 5 2 | addcld | |
7 | 5 2 | pncand | |
8 | 7 3 | eqtrd | |
9 | 6 1 2 8 | subcan2d |