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

Step	Hyp	Ref	Expression
1		wov.1	. 2 ⊢ F:(α → (β → γ))
2		wov.2	. 2 ⊢ A:α
3		wov.3	. 2 ⊢ B:β
4	1, 2, 3	ax-wov 71	1 ⊢ [AFB]:γ

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