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