wct - Higher-Order Logic Explorer

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

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):∗

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