| Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > ILE Home > Th. List > 1pi | Unicode version | ||
| Description: Ordinal 'one' is a positive integer. (Contributed by NM, 29-Oct-1995.) |
| Ref | Expression |
|---|---|
| 1pi |
|
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | 1onn 6606 |
. 2
| |
| 2 | 1n0 6518 |
. 2
| |
| 3 | elni 7421 |
. 2
| |
| 4 | 1, 2, 3 | mpbir2an 945 |
1
|
| Colors of variables: wff set class |
| Syntax hints: |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 106 ax-ia2 107 ax-ia3 108 ax-in1 615 ax-in2 616 ax-io 711 ax-5 1470 ax-7 1471 ax-gen 1472 ax-ie1 1516 ax-ie2 1517 ax-8 1527 ax-10 1528 ax-11 1529 ax-i12 1530 ax-bndl 1532 ax-4 1533 ax-17 1549 ax-i9 1553 ax-ial 1557 ax-i5r 1558 ax-13 2178 ax-14 2179 ax-ext 2187 ax-sep 4162 ax-nul 4170 ax-pow 4218 ax-pr 4253 ax-un 4480 |
| This theorem depends on definitions: df-bi 117 df-3an 983 df-tru 1376 df-nf 1484 df-sb 1786 df-clab 2192 df-cleq 2198 df-clel 2201 df-nfc 2337 df-ne 2377 df-ral 2489 df-rex 2490 df-v 2774 df-dif 3168 df-un 3170 df-in 3172 df-ss 3179 df-nul 3461 df-pw 3618 df-sn 3639 df-pr 3640 df-uni 3851 df-int 3886 df-suc 4418 df-iom 4639 df-1o 6502 df-ni 7417 |
| This theorem is referenced by: mulidpi 7431 1lt2pi 7453 nlt1pig 7454 indpi 7455 1nq 7479 1qec 7501 mulidnq 7502 1lt2nq 7519 archnqq 7530 prarloclemarch 7531 prarloclemarch2 7532 nnnq 7535 ltnnnq 7536 nq0m0r 7569 nq0a0 7570 addpinq1 7577 nq02m 7578 prarloclemlt 7606 prarloclemlo 7607 prarloclemn 7612 prarloclemcalc 7615 nqprm 7655 caucvgprlemm 7781 caucvgprprlemml 7807 caucvgprprlemmu 7808 caucvgsrlemasr 7903 caucvgsr 7915 nntopi 8007 |
| Copyright terms: Public domain | W3C validator |