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

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