Theorem 6nn

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

	Ref	Expression
Assertion	6nn	⊢ 6 ∈ ℕ

Proof

Step	Hyp	Ref	Expression
1		df-6	⊢ 6 = ( 5 + 1 )
2		5nn	⊢ 5 ∈ ℕ
3		peano2nn	⊢ ( 5 ∈ ℕ → ( 5 + 1 ) ∈ ℕ )
4	2 3	ax-mp	⊢ ( 5 + 1 ) ∈ ℕ
5	1 4	eqeltri	⊢ 6 ∈ ℕ