Metamath Proof Explorer

Theorem 7nn

Description: 7 is a positive integer. (Contributed by Mario Carneiro, 15-Sep-2013)

Ref Expression
Assertion 7nn 
|- 7 e. NN

Proof

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