![]() |
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 1425 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | 1 | nfi 1392 |
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 104 ax-ia2 105 ax-ia3 106 ax-gen 1379 ax-ie1 1423 |
This theorem depends on definitions: df-bi 115 df-nf 1391 |
This theorem is referenced by: nf3 1600 sb4or 1756 nfmo1 1955 euexex 2028 2moswapdc 2033 nfre1 2413 ceqsexg 2733 morex 2787 sbc6g 2850 rgenm 3365 intab 3691 nfopab1 3873 nfopab2 3874 copsexg 4034 copsex2t 4035 copsex2g 4036 eusv2nf 4241 onintonm 4296 mosubopt 4460 dmcoss 4659 imadif 5046 funimaexglem 5049 nfoprab1 5632 nfoprab2 5633 nfoprab3 5634 exmidfodomrlemr 6730 exmidfodomrlemrALT 6731 |
Copyright terms: Public domain | W3C validator |