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