![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > hba1 | Unicode version |
Description: ![]() ![]() ![]() ![]() |
Ref | Expression |
---|---|
hba1 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ax-ial 1545 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff set class |
Syntax hints: ![]() ![]() |
This theorem was proved from axioms: ax-ial 1545 |
This theorem is referenced by: nfa1 1552 a5i 1554 hba2 1562 hbia1 1563 19.21h 1568 19.21ht 1592 exim 1610 19.12 1676 19.38 1687 ax9o 1709 equveli 1770 nfald 1771 equs5a 1805 ax11v2 1831 equs5 1840 equs5or 1841 sb56 1897 hbsb4t 2025 hbeu1 2048 eupickbi 2120 moexexdc 2122 2eu4 2131 exists2 2135 hbra1 2520 |
Copyright terms: Public domain | W3C validator |