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:(α → β)
wc.2	⊢ T:α

Assertion

Ref	Expression
ax-wc	⊢ (FT):β

Detailed syntax breakdown of Axiom ax-wc

Step	Hyp	Ref	Expression
1		hbe	. 2 type β
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):β

This axiom is referenced by:  wc  50