Higher-Order Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > HOLE Home > Th. List > wov | Unicode version |
Description: Type of an infix operator. |
Ref | Expression |
---|---|
wov.1 | |
wov.2 | |
wov.3 |
Ref | Expression |
---|---|
wov |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | hga | . 2 type | |
2 | ta | . . 3 term | |
3 | tb | . . 3 term | |
4 | tf | . . 3 term | |
5 | 2, 3, 4 | kbr 9 | . 2 term |
6 | 1, 5 | wffMMJ2t 12 | 1 wff |
Colors of variables: type var term |
This definition is referenced by: dfov2 67 weqi 68 oveq123 88 hbov 101 ovl 107 wan 126 wim 127 wnot 128 wex 129 wor 130 exval 133 notval 135 imval 136 orval 137 anval 138 dfan2 144 hbct 145 ex 148 notval2 149 ecase 153 olc 154 orc 155 exlimdv2 156 exlimdv 157 ax4e 158 eta 166 exlimd 171 ac 184 exmid 186 ax2 191 ax3 192 ax5 194 ax10 200 ax11 201 axrep 207 axpow 208 axun 209 |
Copyright terms: Public domain | W3C validator |