![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > 1onn | Unicode version |
Description: One is a natural number. (Contributed by NM, 29-Oct-1995.) |
Ref | Expression |
---|---|
1onn |
![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | df-1o 6267 |
. 2
![]() ![]() ![]() ![]() ![]() | |
2 | peano1 4468 |
. . 3
![]() ![]() ![]() ![]() | |
3 | peano2 4469 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
4 | 2, 3 | ax-mp 7 |
. 2
![]() ![]() ![]() ![]() ![]() |
5 | 1, 4 | eqeltri 2187 |
1
![]() ![]() ![]() ![]() |
Colors of variables: wff set class |
Syntax hints: ![]() ![]() ![]() ![]() ![]() |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 ax-in1 586 ax-in2 587 ax-io 681 ax-5 1406 ax-7 1407 ax-gen 1408 ax-ie1 1452 ax-ie2 1453 ax-8 1465 ax-10 1466 ax-11 1467 ax-i12 1468 ax-bndl 1469 ax-4 1470 ax-13 1474 ax-14 1475 ax-17 1489 ax-i9 1493 ax-ial 1497 ax-i5r 1498 ax-ext 2097 ax-sep 4006 ax-nul 4014 ax-pow 4058 ax-pr 4091 ax-un 4315 |
This theorem depends on definitions: df-bi 116 df-3an 947 df-tru 1317 df-nf 1420 df-sb 1719 df-clab 2102 df-cleq 2108 df-clel 2111 df-nfc 2244 df-ral 2395 df-rex 2396 df-v 2659 df-dif 3039 df-un 3041 df-in 3043 df-ss 3050 df-nul 3330 df-pw 3478 df-sn 3499 df-pr 3500 df-uni 3703 df-int 3738 df-suc 4253 df-iom 4465 df-1o 6267 |
This theorem is referenced by: 2onn 6371 nnm2 6375 nnaordex 6377 snfig 6662 snnen2og 6706 1nen2 6708 unfiexmid 6759 en1eqsn 6788 omp1eomlem 6931 fodjum 6968 fodju0 6969 en2eleq 6999 en2other2 7000 exmidfodomrlemr 7006 exmidfodomrlemrALT 7007 1pi 7071 1lt2pi 7096 archnqq 7173 nq0m0r 7212 nq02m 7221 prarloclemlt 7249 prarloclemlo 7250 1tonninf 10106 hash2 10451 pwle2 12885 peano3nninf 12893 nninfall 12896 nninfsellemdc 12898 nninfsellemeq 12902 nninfsellemeqinf 12904 nninffeq 12908 sbthom 12913 isomninnlem 12917 |
Copyright terms: Public domain | W3C validator |