![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > nfe1 | Unicode version |
Description: ![]() ![]() ![]() ![]() |
Ref | Expression |
---|---|
nfe1 |
![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | hbe1 1381 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | 1 | nfi 1348 |
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-gen 1335 ax-ie1 1379 |
This theorem depends on definitions: df-bi 110 df-nf 1347 |
This theorem is referenced by: nf3 1556 sb4or 1711 nfmo1 1909 euexex 1982 2moswapdc 1987 nfre1 2359 ceqsexg 2666 morex 2719 sbc6g 2782 rgenm 3317 intab 3635 nfopab1 3817 nfopab2 3818 copsexg 3972 copsex2t 3973 copsex2g 3974 eusv2nf 4154 mosubopt 4348 dmcoss 4544 imadif 4922 funimaexglem 4925 nfoprab1 5496 nfoprab2 5497 nfoprab3 5498 |
Copyright terms: Public domain | W3C validator |