| Metamath Proof Explorer |
< Previous
Next >
Related theorems Unicode version |
| Description: The successor of any natural number is not zero. One of Peano's 5 postulates for arithmetic. Proposition 7.30(3) of [TakeutiZaring] p. 42. |
| Ref | Expression |
|---|---|
| peano3 |
|
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | nsuceq0 3561 |
. 2
| |
| 2 | 1 | a1i 8 |
1
|
| Colors of variables: wff set class |
| Syntax hints: |
| This theorem was proved from axioms: ax-1 4 ax-2 5 ax-3 6 ax-mp 7 ax-7 1142 ax-gen 1143 ax-8 1144 ax-9 1145 ax-10 1146 ax-11 1147 ax-12 1148 ax-17 1155 ax-4 1157 ax-5o 1159 ax-6o 1162 ax-9o 1319 ax-10o 1338 ax-16 1418 ax-11o 1426 ax-ext 1702 ax-nul 3260 |
| This theorem depends on definitions: df-bi 163 df-or 240 df-an 241 df-ex 1165 df-sb 1374 df-clab 1709 df-cleq 1714 df-clel 1717 df-ne 1856 df-v 2127 df-dif 2430 df-un 2433 df-nul 2702 df-sn 2873 df-suc 3478 |