Theorem wctr 34

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
wctr	⊢ T:∗

Proof of Theorem wctr

Step	Hyp	Ref	Expression
1		wctl.1	. 2 ⊢ (S, T):∗
2	1	ax-wctr 32	1 ⊢ T:∗

Syntax hints:  ∗hb 3  kct 10  wffMMJ2t 12

This theorem was proved from axioms:  ax-wctr 32

This theorem is referenced by:  syldan  36  simpld  37  simprd  38  trul  39  ancoms  54  sylan  59  an32s  60  anassrs  62  ex  158  con2d  161  exlimdv  167  exlimd  183  alimdv  184