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

Step	Hyp	Ref	Expression
1		hga	. 2 type γ
2		ta	. . 3 term A
3		tb	. . 3 term B
4		tf	. . 3 term F
5	2, 3, 4	kbr 9	. 2 term [AFB]
6	1, 5	wffMMJ2t 12	1 wff [AFB]:γ

This axiom is referenced by:  wov  72