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

Theorem wov 72
Description: Type of an infix operator. (Contributed by Mario Carneiro, 8-Oct-2014.)
Hypotheses
Ref Expression
wov.1 F:(α → (βγ))
wov.2 A:α
wov.3 B:β
Assertion
Ref Expression
wov [AFB]:γ

Proof of Theorem wov
StepHypRef Expression
1 wov.1 . 2 F:(α → (βγ))
2 wov.2 . 2 A:α
3 wov.3 . 2 B:β
41, 2, 3ax-wov 71 1 [AFB]:γ
Colors of variables: type var term
Syntax hints:  ht 2  [kbr 9  wffMMJ2t 12
This theorem was proved from axioms:  ax-wov 71
This theorem is referenced by:  dfov2  75  weqi  76  oveq123  98  hbov  111  ovl  117  wan  136  wim  137  wnot  138  wex  139  wor  140  exval  143  notval  145  imval  146  orval  147  anval  148  dfan2  154  hbct  155  ex  158  notval2  159  ecase  163  olc  164  orc  165  exlimdv2  166  exlimdv  167  ax4e  168  eta  178  exlimd  183  ac  197  exmid  199  ax2  204  ax3  205  ax5  207  ax10  213  ax11  214  axrep  220  axpow  221  axun  222
  Copyright terms: Public domain W3C validator