![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > nfcri | Unicode version |
Description: Consequence of the
not-free predicate. (Note that unlike nfcr 2324, this
does not require ![]() ![]() |
Ref | Expression |
---|---|
nfcri.1 |
![]() ![]() ![]() ![]() |
Ref | Expression |
---|---|
nfcri |
![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | nfcri.1 |
. . 3
![]() ![]() ![]() ![]() | |
2 | 1 | nfcrii 2325 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
3 | 2 | nfi 1473 |
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-io 710 ax-5 1458 ax-7 1459 ax-gen 1460 ax-ie1 1504 ax-ie2 1505 ax-8 1515 ax-10 1516 ax-11 1517 ax-i12 1518 ax-bndl 1520 ax-4 1521 ax-17 1537 ax-i9 1541 ax-ial 1545 ax-i5r 1546 ax-ext 2171 |
This theorem depends on definitions: df-bi 117 df-nf 1472 df-sb 1774 df-cleq 2182 df-clel 2185 df-nfc 2321 |
This theorem is referenced by: clelsb1f 2336 nfnfc 2339 nfeq 2340 nfel 2341 cleqf 2357 sbabel 2359 r2alf 2507 r2exf 2508 nfrabxy 2671 cbvralfw 2708 cbvrexfw 2709 cbvralf 2710 cbvrexf 2711 cbvrab 2750 rmo3f 2949 nfccdeq 2975 sbcabel 3059 cbvcsbw 3076 cbvcsb 3077 cbvralcsf 3134 cbvrexcsf 3135 cbvreucsf 3136 cbvrabcsf 3137 dfss2f 3161 nfdif 3271 nfun 3306 nfin 3356 nfop 3809 nfiunxy 3927 nfiinxy 3928 nfiunya 3929 nfiinya 3930 cbviun 3938 cbviin 3939 iunxsngf 3979 cbvdisj 4005 nfdisjv 4007 disjiun 4013 nfmpt 4110 cbvmptf 4112 nffrfor 4366 onintrab2im 4535 tfis 4600 nfxp 4671 opeliunxp 4699 iunxpf 4793 elrnmpt1 4896 fvmptssdm 5621 nfmpo 5965 cbvmpox 5974 fmpox 6225 nffrec 6421 cc3 7297 nfsum1 11396 nfsum 11397 fsum2dlemstep 11474 fisumcom2 11478 nfcprod1 11594 nfcprod 11595 cbvprod 11598 fprod2dlemstep 11662 fprodcom2fi 11666 ctiunctlemudc 12488 ctiunctlemfo 12490 |
Copyright terms: Public domain | W3C validator |