![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > hbe1 | Unicode version |
Description: ![]() ![]() ![]() ![]() |
Ref | Expression |
---|---|
hbe1 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ax-ie1 1379 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff set class |
Syntax hints: ![]() ![]() ![]() |
This theorem was proved from axioms: ax-ie1 1379 |
This theorem is referenced by: nfe1 1382 19.8a 1479 exim 1487 19.43 1516 hbex 1524 excomim 1550 19.38 1563 exan 1580 equs5e 1673 exdistrfor 1678 hbmo1 1935 euan 1953 euor2 1955 eupicka 1977 mopick2 1980 moexexdc 1981 2moex 1983 2euex 1984 2exeu 1989 2eu4 1990 2eu7 1991 |
Copyright terms: Public domain | W3C validator |