Theorem peano2zd

Description: Deduction from second Peano postulate generalized to integers. (Contributed by Mario Carneiro, 28-May-2016)

	Ref	Expression
Hypothesis	zred.1	⊢ ( 𝜑 → 𝐴 ∈ ℤ )
Assertion	peano2zd	⊢ ( 𝜑 → ( 𝐴 + 1 ) ∈ ℤ )

Proof

Step	Hyp	Ref	Expression
1		zred.1	⊢ ( 𝜑 → 𝐴 ∈ ℤ )
2		peano2z	⊢ ( 𝐴 ∈ ℤ → ( 𝐴 + 1 ) ∈ ℤ )
3	1 2	syl	⊢ ( 𝜑 → ( 𝐴 + 1 ) ∈ ℤ )