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

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

Detailed syntax breakdown of Axiom ax-wov
StepHypRef Expression
1 hga . 2 type γ
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]:γ
Colors of variables: type var term
This axiom is referenced by:  wov  72
  Copyright terms: Public domain W3C validator