Metamath Proof Explorer

Theorem nngt0i

Description: A positive integer is positive (inference version). (Contributed by NM, 17-Sep-1999)

Ref Expression
Hypothesis nngt0.1 
|- A e. NN
Assertion nngt0i 
|- 0 < A

Proof

Step Hyp Ref Expression
1 nngt0.1 
 |-  A e. NN
2 nngt0 
 |-  ( A e. NN -> 0 < A )
3 1 2 ax-mp 
 |-  0 < A