HOLE Home Higher-Order Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  HOLE Home  >  Th. List  >  wov Unicode version

Definition wov 64
Description: Type of an infix operator.
Hypotheses
Ref Expression
wov.1 |- F:(al -> (be -> ga))
wov.2 |- A:al
wov.3 |- B:be
Assertion
Ref Expression
wov |- [AFB]:ga

Detailed syntax breakdown of Definition wov
StepHypRef Expression
1 hga . 2 type ga
2 ta . . 3 term A
3 tb . . 3 term B
4 tf . . 3 term F
52, 3, 4kbr 9 . 2 term [AFB]
61, 5wffMMJ2t 12 1 wff [AFB]:ga
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