Higher-Order Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > HOLE Home > Th. List > wal | Unicode version |
Description: For all type. |
Ref | Expression |
---|---|
wal |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | wv 58 | . . . 4 | |
2 | wtru 40 | . . . . 5 | |
3 | 2 | wl 59 | . . . 4 |
4 | 1, 3 | weqi 68 | . . 3 |
5 | 4 | wl 59 | . 2 |
6 | df-al 116 | . 2 | |
7 | 5, 6 | eqtypri 71 | 1 |
Colors of variables: type var term |
Syntax hints: tv 1 ht 2 hb 3 kl 6 ke 7 kt 8 kbr 9 wffMMJ2t 12 tal 112 |
This theorem was proved from axioms: ax-cb1 29 ax-refl 39 |
This theorem depends on definitions: df-al 116 |
This theorem is referenced by: wfal 125 wex 129 wor 130 weu 131 alval 132 exval 133 euval 134 orval 137 ax4g 139 exlimdv2 156 ax4e 158 exlimd 171 alimdv 172 alnex 174 exnal1 175 ac 184 exnal 188 ax5 194 ax6 195 ax7 196 ax9 199 ax10 200 ax11 201 ax12 202 axext 206 axrep 207 axpow 208 axun 209 |
Copyright terms: Public domain | W3C validator |