Description: Deduction from second Peano postulate generalized to integers. (Contributed by Mario Carneiro, 28May2016)
Ref  Expression  

Hypothesis  zred.1   ( ph > A e. ZZ ) 

Assertion  peano2zd   ( ph > ( A + 1 ) e. ZZ ) 
Step  Hyp  Ref  Expression 

1  zred.1   ( ph > A e. ZZ ) 

2  peano2z   ( A e. ZZ > ( A + 1 ) e. ZZ ) 

3  1 2  syl   ( ph > ( A + 1 ) e. ZZ ) 