Metamath Proof Explorer

Theorem 2nn

Description: 2 is a positive integer. (Contributed by NM, 20-Aug-2001)

Ref Expression
Assertion 2nn 
|- 2 e. NN

Proof

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