Theorem nngt0i

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

	Ref	Expression
Hypothesis	nngt0.1	$$⊢A\in \mathbb{N}$$
Assertion	nngt0i	$$⊢0<A$$

Proof

Step	Hyp	Ref	Expression
1		nngt0.1	$$⊢A\in \mathbb{N}$$
2		nngt0	$$⊢A\in \mathbb{N}\to 0<A$$
3	1 2	ax-mp	$$⊢0<A$$