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:(al -> (be -> ga))
wov.2	|- A:al
wov.3	|- B:be

Assertion

Ref	Expression
ax-wov	|- [AFB]:ga

Detailed syntax breakdown of Axiom ax-wov

Step	Hyp	Ref	Expression
1		hga	. 2 type ga
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]:ga

This axiom is referenced by:  wov  72