Description: Subtracting 2 and afterwards 1 from a number results in the difference between the number and 3. (Contributed by Alexander van der Vekens, 16-Sep-2018)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | cnm2m1cnm3 | 
| Step | Hyp | Ref | Expression | 
|---|---|---|---|
| 1 | id | ||
| 2 | 2cnd | ||
| 3 | 1cnd | ||
| 4 | 1 2 3 | subsub4d | |
| 5 | 2p1e3 | ||
| 6 | 5 | a1i | |
| 7 | 6 | oveq2d | |
| 8 | 4 7 | eqtrd |