Theorem 10nn

Description: 10 is a positive integer. (Contributed by NM, 8-Nov-2012) (Revised by AV, 6-Sep-2021)

	Ref	Expression
Assertion	10nn	$$⊢10\in \mathbb{N}$$

Proof

Step	Hyp	Ref	Expression
1		9p1e10	$$⊢9+1=10$$
2		9nn	$$⊢9\in \mathbb{N}$$
3		peano2nn	$$⊢9\in \mathbb{N}\to 9+1\in \mathbb{N}$$
4	2 3	ax-mp	$$⊢9+1\in \mathbb{N}$$
5	1 4	eqeltrri	$$⊢10\in \mathbb{N}$$