Metamath Proof Explorer

Theorem peano2

Description: The successor of any natural number is a natural number. One of Peano's five postulates for arithmetic. Proposition 7.30(2) of TakeutiZaring p. 42. (Contributed by NM, 3-Sep-2003)

Ref Expression
Assertion peano2 A ω suc A ω


Step Hyp Ref Expression
1 peano2b A ω suc A ω
2 1 biimpi A ω suc A ω