Metamath Proof Explorer


Theorem 4nn

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

Ref Expression
Assertion 4nn 4

Proof

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