![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > pinn | Unicode version |
Description: A positive integer is a natural number. (Contributed by NM, 15-Aug-1995.) |
Ref | Expression |
---|---|
pinn |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | df-ni 7136 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | difss 3207 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
3 | 1, 2 | eqsstri 3134 |
. 2
![]() ![]() ![]() ![]() |
4 | 3 | sseli 3098 |
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 105 ax-ia2 106 ax-ia3 107 ax-in1 604 ax-in2 605 ax-io 699 ax-5 1424 ax-7 1425 ax-gen 1426 ax-ie1 1470 ax-ie2 1471 ax-8 1483 ax-10 1484 ax-11 1485 ax-i12 1486 ax-bndl 1487 ax-4 1488 ax-17 1507 ax-i9 1511 ax-ial 1515 ax-i5r 1516 ax-ext 2122 |
This theorem depends on definitions: df-bi 116 df-tru 1335 df-nf 1438 df-sb 1737 df-clab 2127 df-cleq 2133 df-clel 2136 df-nfc 2271 df-v 2691 df-dif 3078 df-in 3082 df-ss 3089 df-ni 7136 |
This theorem is referenced by: pion 7142 piord 7143 elni2 7146 mulidpi 7150 ltsopi 7152 pitric 7153 pitri3or 7154 ltdcpi 7155 addclpi 7159 mulclpi 7160 addcompig 7161 addasspig 7162 mulcompig 7163 mulasspig 7164 distrpig 7165 addcanpig 7166 mulcanpig 7167 addnidpig 7168 ltexpi 7169 ltapig 7170 ltmpig 7171 nnppipi 7175 enqdc 7193 archnqq 7249 prarloclemarch2 7251 enq0enq 7263 enq0sym 7264 enq0ref 7265 enq0tr 7266 nqnq0pi 7270 nqnq0 7273 addcmpblnq0 7275 mulcmpblnq0 7276 mulcanenq0ec 7277 addclnq0 7283 nqpnq0nq 7285 nqnq0a 7286 nqnq0m 7287 nq0m0r 7288 nq0a0 7289 nnanq0 7290 distrnq0 7291 mulcomnq0 7292 addassnq0lemcl 7293 addassnq0 7294 nq02m 7297 prarloclemlt 7325 prarloclemn 7331 |
Copyright terms: Public domain | W3C validator |