wct - Higher-Order Logic Explorer

	Higher-Order Logic Explorer		< Previous Next > Nearby theorems
Mirrors > Home > HOLE Home > Th. List > wct		Unicode version

Definition wct 44

Description: The type of a context.

**Hypotheses**
Ref	Expression
wct.1
wct.2

**Assertion**
Ref	Expression
wct

**Detailed syntax breakdown of Definition wct**
Step	Hyp	Ref	Expression
1		hb 3	. 2 type
2		ts	. . 3 term
3		tt	. . 3 term
4	2, 3	kct 10	. 2 term
5	1, 4	wffMMJ2t 12	1 wff

Colors of variables: type var term

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