Theorem wctl 33

Description: Reverse closure for the type of a context. (This axiom is unnecessary; see ax-cb1 29.) (Contributed by Mario Carneiro, 8-Oct-2014.)

Hypothesis

Ref	Expression
wctl.1	|- (S, T):*

Assertion

Ref	Expression
wctl	|- S:*

Proof of Theorem wctl

Step	Hyp	Ref	Expression
1		wctl.1	. 2 |- (S, T):*
2	1	ax-wctl 31	1 |- S:*

Syntax hints:  *hb 3  kct 10  wffMMJ2t 12

This theorem was proved from axioms:  ax-wctl 31

This theorem is referenced by:  syldan  36  simpld  37  simprd  38  ancoms  54  an32s  60  anasss  61  anassrs  62  hbxfrf  107  ex  158  con2d  161  exlimdv2  166  exlimd  183  alimdv  184  eximdv  185