Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > hbe1 | Unicode version |
Description: is not free in . (Contributed by NM, 5-Aug-1993.) |
Ref | Expression |
---|---|
hbe1 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ax-ie1 1382 | 1 |
Colors of variables: wff set class |
Syntax hints: wi 4 wal 1241 wex 1381 |
This theorem was proved from axioms: ax-ie1 1382 |
This theorem is referenced by: nfe1 1385 19.8a 1482 exim 1490 19.43 1519 hbex 1527 excomim 1553 19.38 1566 exan 1583 equs5e 1676 exdistrfor 1681 hbmo1 1938 euan 1956 euor2 1958 eupicka 1980 mopick2 1983 moexexdc 1984 2moex 1986 2euex 1987 2exeu 1992 2eu4 1993 2eu7 1994 |
Copyright terms: Public domain | W3C validator |