Higher-Order Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > HOLE Home > Th. List > wim | Unicode version |
Description: Implication type. |
Ref | Expression |
---|---|
wim |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | wan 126 | . . . . . 6 | |
2 | wv 58 | . . . . . 6 | |
3 | wv 58 | . . . . . 6 | |
4 | 1, 2, 3 | wov 64 | . . . . 5 |
5 | 4, 2 | weqi 68 | . . . 4 |
6 | 5 | wl 59 | . . 3 |
7 | 6 | wl 59 | . 2 |
8 | df-im 119 | . 2 | |
9 | 7, 8 | 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 tan 109 tim 111 |
This theorem was proved from axioms: ax-cb1 29 ax-refl 39 |
This theorem depends on definitions: df-an 118 df-im 119 |
This theorem is referenced by: wnot 128 wex 129 wor 130 exval 133 notval 135 imval 136 orval 137 notval2 149 ecase 153 olc 154 orc 155 exlimdv2 156 exlimdv 157 ax4e 158 exlimd 171 ac 184 ax2 191 ax3 192 ax5 194 ax11 201 axrep 207 axpow 208 axun 209 |
Copyright terms: Public domain | W3C validator |