Axiom ax-wc 49

Description: The type of a combination. (Contributed by Mario Carneiro, 7-Oct-2014.) (New usage is discouraged.)

Hypotheses

Ref	Expression
wc.1	|- F:(al -> be)
wc.2	|- T:al

Assertion

Ref	Expression
ax-wc	|- (FT):be

Detailed syntax breakdown of Axiom ax-wc

Step	Hyp	Ref	Expression
1		hbe	. 2 type be
2		tf	. . 3 term F
3		tt	. . 3 term T
4	2, 3	kc 5	. 2 term (FT)
5	1, 4	wffMMJ2t 12	1 wff (FT):be

This axiom is referenced by:  wc  50