Higher-Order Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > HOLE Home > Th. List > wtru | GIF version |
Description: Truth type. |
Ref | Expression |
---|---|
wtru | ⊢ ⊤:∗ |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | weq 38 | . . 3 ⊢ = :(∗ → (∗ → ∗)) | |
2 | 1 | ax-refl 39 | . 2 ⊢ ⊤⊧(( = = ) = ) |
3 | 2 | ax-cb1 29 | 1 ⊢ ⊤:∗ |
Colors of variables: type var term |
Syntax hints: → ht 2 ∗hb 3 kc 5 = ke 7 ⊤kt 8 wffMMJ2t 12 |
This theorem was proved from axioms: ax-cb1 29 ax-refl 39 |
This theorem is referenced by: tru 41 dedi 75 eqtru 76 hbth 99 hbov 101 ovl 107 wal 124 wan 126 alval 132 anval 138 alrimiv 141 dfan2 144 hbct 145 olc 154 orc 155 alrimi 170 exlimd 171 alnex 174 exnal1 175 dfex2 185 exmid 186 ax1 190 ax2 191 ax3 192 ax5 194 ax7 196 ax8 198 ax9 199 ax10 200 ax11 201 ax13 203 ax14 204 axext 206 axrep 207 axpow 208 axun 209 |
Copyright terms: Public domain | W3C validator |