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