Metamath Proof Explorer


Theorem 7nn

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

Ref Expression
Assertion 7nn 7

Proof

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