![]() |
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 1384 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | 1 | nfi 1351 |
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 1338 ax-ie1 1382 |
This theorem depends on definitions: df-bi 110 df-nf 1350 |
This theorem is referenced by: nf3 1559 sb4or 1714 nfmo1 1912 euexex 1985 2moswapdc 1990 nfre1 2365 ceqsexg 2672 morex 2725 sbc6g 2788 rgenm 3323 intab 3644 nfopab1 3826 nfopab2 3827 copsexg 3981 copsex2t 3982 copsex2g 3983 eusv2nf 4188 onintonm 4243 mosubopt 4405 dmcoss 4601 imadif 4979 funimaexglem 4982 nfoprab1 5554 nfoprab2 5555 nfoprab3 5556 |
Copyright terms: Public domain | W3C validator |