HOLE Home Higher-Order Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  HOLE Home  >  Th. List  >  wctr GIF version

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
StepHypRef Expression
1 wctl.1 . 2 (S, T):∗
21ax-wctr 32 1 T:∗
Colors of variables: type var term
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
  Copyright terms: Public domain W3C validator