| 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 2340, this
does not require |
| Ref | Expression |
|---|---|
| nfcri.1 |
|
| Ref | Expression |
|---|---|
| nfcri |
|
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | nfcri.1 |
. . 3
| |
| 2 | 1 | nfcrii 2341 |
. 2
|
| 3 | 2 | nfi 1485 |
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 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-ext 2187 |
| This theorem depends on definitions: df-bi 117 df-nf 1484 df-sb 1786 df-cleq 2198 df-clel 2201 df-nfc 2337 |
| This theorem is referenced by: clelsb1f 2352 nfnfc 2355 nfeq 2356 nfel 2357 cleqf 2373 sbabel 2375 r2alf 2523 r2exf 2524 nfrabw 2687 cbvralfw 2728 cbvrexfw 2729 cbvralf 2730 cbvrexf 2731 cbvrab 2770 rmo3f 2970 nfccdeq 2996 sbcabel 3080 cbvcsbw 3097 cbvcsb 3098 cbvralcsf 3156 cbvrexcsf 3157 cbvreucsf 3158 cbvrabcsf 3159 dfss2f 3184 nfdif 3294 nfun 3329 nfin 3379 nfop 3835 nfiunxy 3953 nfiinxy 3954 nfiunya 3955 nfiinya 3956 cbviun 3964 cbviin 3965 iunxsngf 4005 cbvdisj 4031 nfdisjv 4033 disjiun 4039 nfmpt 4136 cbvmptf 4138 nffrfor 4395 onintrab2im 4566 tfis 4631 nfxp 4702 opeliunxp 4730 iunxpf 4826 elrnmpt1 4929 fvmptssdm 5664 nfmpo 6014 cbvmpox 6023 fmpox 6286 nffrec 6482 cc3 7380 nfsum1 11667 nfsum 11668 fsum2dlemstep 11745 fisumcom2 11749 nfcprod1 11865 nfcprod 11866 cbvprod 11869 fprod2dlemstep 11933 fprodcom2fi 11937 ctiunctlemudc 12808 ctiunctlemfo 12810 |
| Copyright terms: Public domain | W3C validator |