This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem 9nn

Description: 9 is a positive integer. (Contributed by NM, 21-Oct-2012)

		Ref	Expression
	Assertion	9nn	$⊢ 9 \in ℕ$

Step	Hyp	Ref	Expression
1		df-9	$⊢ 9 = 8 + 1$
2		8nn	$⊢ 8 \in ℕ$
3		peano2nn	$⊢ 8 \in ℕ \to 8 + 1 \in ℕ$
4	2 3	ax-mp	$⊢ 8 + 1 \in ℕ$
5	1 4	eqeltri	$⊢ 9 \in ℕ$