![]() |
New Foundations Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > NFE Home > Th. List > hbn1 | Unicode version |
Description: ![]() ![]() ![]() ![]() ![]() |
Ref | Expression |
---|---|
hbn1 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ax-6 1729 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff setvar class |
Syntax hints: ![]() ![]() ![]() |
This theorem was proved from axioms: ax-6 1729 |
This theorem is referenced by: hbe1 1731 modal-5 1733 ax5o 1749 hbnOLD 1777 hba1OLD 1787 hbimdOLD 1816 dvelimhw 1849 ax12olem6 1932 dvelimv 1939 a16g 1945 ax15 2021 dvelimALT 2133 ax11indn 2195 |
Copyright terms: Public domain | W3C validator |