![]() |
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 6288 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | difss 3064 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
3 | 1, 2 | eqsstri 2969 |
. 2
![]() ![]() ![]() ![]() |
4 | 3 | sseli 2935 |
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 99 ax-ia2 100 ax-ia3 101 ax-in1 544 ax-in2 545 ax-io 629 ax-5 1333 ax-7 1334 ax-gen 1335 ax-ie1 1379 ax-ie2 1380 ax-8 1392 ax-10 1393 ax-11 1394 ax-i12 1395 ax-bndl 1396 ax-4 1397 ax-17 1416 ax-i9 1420 ax-ial 1424 ax-i5r 1425 ax-ext 2019 |
This theorem depends on definitions: df-bi 110 df-tru 1245 df-nf 1347 df-sb 1643 df-clab 2024 df-cleq 2030 df-clel 2033 df-nfc 2164 df-v 2553 df-dif 2914 df-in 2918 df-ss 2925 df-ni 6288 |
This theorem is referenced by: pion 6294 piord 6295 elni2 6298 mulidpi 6302 ltsopi 6304 pitric 6305 pitri3or 6306 ltdcpi 6307 addclpi 6311 mulclpi 6312 addcompig 6313 addasspig 6314 mulcompig 6315 mulasspig 6316 distrpig 6317 addcanpig 6318 mulcanpig 6319 addnidpig 6320 ltexpi 6321 ltapig 6322 ltmpig 6323 nnppipi 6327 enqdc 6345 archnqq 6400 prarloclemarch2 6402 enq0enq 6414 enq0sym 6415 enq0ref 6416 enq0tr 6417 nqnq0pi 6421 nqnq0 6424 addcmpblnq0 6426 mulcmpblnq0 6427 mulcanenq0ec 6428 addclnq0 6434 nqpnq0nq 6436 nqnq0a 6437 nqnq0m 6438 nq0m0r 6439 nq0a0 6440 nnanq0 6441 distrnq0 6442 mulcomnq0 6443 addassnq0lemcl 6444 addassnq0 6445 nq02m 6448 prarloclemlt 6476 prarloclemn 6482 |
Copyright terms: Public domain | W3C validator |