Metamath Proof Explorer

Theorem 9nn

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

Ref Expression
Assertion 9nn 
|- 9 e. NN

Proof

Step Hyp Ref Expression
1 df-9 
 |-  9 = ( 8 + 1 )
2 8nn 
 |-  8 e. NN
3 peano2nn 
 |-  ( 8 e. NN -> ( 8 + 1 ) e. NN )
4 2 3 ax-mp 
 |-  ( 8 + 1 ) e. NN
5 1 4 eqeltri 
 |-  9 e. NN