Metamath Proof Explorer


Theorem 3nn

Description: 3 is a positive integer. (Contributed by NM, 8-Jan-2006)

Ref Expression
Assertion 3nn 3

Proof

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