Theorem peano2nn0

Description: Second Peano postulate for nonnegative integers. (Contributed by NM, 9-May-2004)

	Ref	Expression
Assertion	peano2nn0	$$⊢N\in {\mathbb{N}}_0\to N+1\in {\mathbb{N}}_0$$

Proof

Step	Hyp	Ref	Expression
1		1nn0	$$⊢1\in {\mathbb{N}}_0$$
2		nn0addcl	$$⊢\left(N\in {\mathbb{N}}_0\wedge 1\in {\mathbb{N}}_0\right)\to N+1\in {\mathbb{N}}_0$$
3	1 2	mpan2	$$⊢N\in {\mathbb{N}}_0\to N+1\in {\mathbb{N}}_0$$