Description: Multiplication with successor. Theorem 4J(A2) of Enderton p. 80. (Contributed by NM, 20-Sep-1995) (Revised by Mario Carneiro, 14-Nov-2014)
Ref | Expression | ||
---|---|---|---|
Assertion | nnmsuc | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | nnon | |
|
2 | onmsuc | |
|
3 | 1 2 | sylan | |