Axiom ax-wct 47

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

Hypotheses

Ref	Expression
wct.1	|- S:*
wct.2	|- T:*

Assertion

Ref	Expression
ax-wct	|- (S, T):*

Detailed syntax breakdown of Axiom ax-wct

Step	Hyp	Ref	Expression
1		hb 3	. 2 type *
2		ts	. . 3 term S
3		tt	. . 3 term T
4	2, 3	kct 10	. 2 term (S, T)
5	1, 4	wffMMJ2t 12	1 wff (S, T):*

This axiom is referenced by:  wct  48