wctl - Higher-Order Logic Explorer

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

Definition wctl 31

Description: Reverse closure for the type of a context. (This axiom is unnecessary; see ax-cb1 29.)

**Hypothesis**
Ref	Expression
wctl.1	⊢ (S, T):∗

**Assertion**
Ref	Expression
wctl	⊢ S:∗

**Detailed syntax breakdown of Definition wctl**
Step	Hyp	Ref	Expression
1		hb 3	. 2 type ∗
2		ts	. 2 term S
3	1, 2	wffMMJ2t 12	1 wff S:∗

Colors of variables: type var term

This definition is referenced by: syldan 34 simpld 35 simprd 36 ancoms 49 an32s 55 anasss 56 anassrs 57 hbxfrf 97 ex 148 con2d 151 exlimdv2 156 exlimd 171 alimdv 172 eximdv 173