![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > nfan | Unicode version |
Description: If ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Ref | Expression |
---|---|
nfan.1 |
![]() ![]() ![]() ![]() |
nfan.2 |
![]() ![]() ![]() ![]() |
Ref | Expression |
---|---|
nfan |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | nfan.1 |
. 2
![]() ![]() ![]() ![]() | |
2 | nfan.2 |
. . 3
![]() ![]() ![]() ![]() | |
3 | 2 | a1i 9 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
4 | 1, 3 | nfan1 1453 |
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-5 1333 ax-gen 1335 ax-4 1397 |
This theorem depends on definitions: df-bi 110 df-nf 1347 |
This theorem is referenced by: nf3an 1455 cbvex2 1794 nfsbxyt 1816 sbcomxyyz 1843 nfsb4t 1887 clelab 2159 nfel 2183 2ralbida 2339 reean 2472 nfrabxy 2484 cbvrexf 2522 cbvreu 2525 cbvrab 2549 ceqsex2 2588 vtocl2gaf 2614 rspce 2645 eqvincf 2663 elrabf 2690 elrab3t 2691 rexab2 2701 morex 2719 reu2 2723 sbc2iegf 2822 rmo2ilem 2841 rmo3 2843 csbiebt 2880 csbie2t 2888 cbvrexcsf 2903 cbvreucsf 2904 cbvrabcsf 2905 nfopd 3557 eluniab 3583 dfnfc2 3589 nfdisjv 3748 nfopab 3816 cbvopab 3819 cbvopab1 3821 cbvopab2 3822 cbvopab1s 3823 mpteq12f 3828 nfmpt 3840 cbvmpt 3842 repizf2 3906 nfpo 4029 nfso 4030 peano2 4261 nfxp 4314 opeliunxp 4338 nfco 4444 elrnmpt1 4528 nfimad 4620 iota2 4836 dffun4f 4861 nffun 4867 imadif 4922 funimaexglem 4925 nffn 4938 nff 4986 nff1 5033 nffo 5048 nff1o 5067 fun11iun 5090 nffvd 5130 fv3 5140 fmptco 5273 nfiso 5389 cbvriota 5421 riota2df 5431 riota5f 5435 nfoprab 5499 mpt2eq123 5506 nfmpt2 5515 cbvoprab1 5518 cbvoprab2 5519 cbvoprab12 5520 cbvoprab3 5522 cbvmpt2x 5524 ovmpt2dxf 5568 opabex3d 5690 opabex3 5691 dfoprab4f 5761 fmpt2x 5768 nfrecs 5863 tfri3 5894 nffrec 5921 erovlem 6134 bdsepnft 9342 bdsepnfALT 9344 bj-findis 9439 strcollnft 9444 |
Copyright terms: Public domain | W3C validator |