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 |