Theorem jm2.27dlem4

Description: Lemma for rmydioph . Infer NN -hood of large numbers. (Contributed by Stefan O'Rear, 11-Oct-2014)

	Ref	Expression
Hypotheses	jm2.27dlem3.1	$$⊢A\in \mathbb{N}$$
	jm2.27dlem4.2	$$⊢B=A+1$$
Assertion	jm2.27dlem4	$$⊢B\in \mathbb{N}$$

Proof

Step	Hyp	Ref	Expression
1		jm2.27dlem3.1	$$⊢A\in \mathbb{N}$$
2		jm2.27dlem4.2	$$⊢B=A+1$$
3		peano2nn	$$⊢A\in \mathbb{N}\to A+1\in \mathbb{N}$$
4	1 3	ax-mp	$$⊢A+1\in \mathbb{N}$$
5	2 4	eqeltri	$$⊢B\in \mathbb{N}$$