Theorem nnne0ALT

Description: Alternate version of nnne0 . A positive integer is nonzero. (Contributed by NM, 27-Sep-1999) (New usage is discouraged.) (Proof modification is discouraged.)

	Ref	Expression
Assertion	nnne0ALT	$$⊢A\in \mathbb{N}\to A\ne 0$$

Proof

Step	Hyp	Ref	Expression
1		0nnnALT	$$⊢\neg 0\in \mathbb{N}$$
2		eleq1	$$⊢A=0\to \left(A\in \mathbb{N}\leftrightarrow 0\in \mathbb{N}\right)$$
3	1 2	mtbiri	$$⊢A=0\to \neg A\in \mathbb{N}$$
4	3	necon2ai	$$⊢A\in \mathbb{N}\to A\ne 0$$