Metamath Proof Explorer


Theorem 9nn

Description: 9 is a positive integer. (Contributed by NM, 21-Oct-2012)

Ref Expression
Assertion 9nn 9

Proof

Step Hyp Ref Expression
1 df-9 9 = 8 + 1
2 8nn 8
3 peano2nn 8 8 + 1
4 2 3 ax-mp 8 + 1
5 1 4 eqeltri 9