Metamath Proof Explorer

Theorem 10nn

Description: 10 is a positive integer. (Contributed by NM, 8-Nov-2012) (Revised by AV, 6-Sep-2021)

Ref Expression
Assertion 10nn 
|- ; 1 0 e. NN

Proof

Step Hyp Ref Expression
1 9p1e10 
 |-  ( 9 + 1 ) = ; 1 0
2 9nn 
 |-  9 e. NN
3 peano2nn 
 |-  ( 9 e. NN -> ( 9 + 1 ) e. NN )
4 2 3 ax-mp 
 |-  ( 9 + 1 ) e. NN
5 1 4 eqeltrri 
 |-  ; 1 0 e. NN