Definition wct 44

Description: The type of a context.

Hypotheses

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

Assertion

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

Detailed syntax breakdown of Definition 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 definition is referenced by:  eqtru  76  hbct  145  ex  148  con2d  151  exlimdv2  156  exmid  186  ax2  191  ax3  192  ax11  201  ax13  203  ax14  204  axun  209