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

Theorem wtru 40
Description: Truth type.
Assertion
Ref Expression
wtru |- T.:*

Proof of Theorem wtru
StepHypRef Expression
1 weq 38 . . 3 |- = :(* -> (* -> *))
21ax-refl 39 . 2 |- T. |= (( = = ) = )
32ax-cb1 29 1 |- T.:*
Colors of variables: type var term
Syntax hints:   -> ht 2  *hb 3  kc 5   = ke 7  T.kt 8  wffMMJ2t 12
This theorem is referenced by:  tru  41  dedi  75  eqtru  76  hbth  99  hbov  101  ovl  107  wal  124  wan  126  alval  132  anval  138  alrimiv  141  dfan2  144  hbct  145  olc  154  orc  155  alrimi  170  exlimd  171  alnex  174  exnal1  175  dfex2  185  exmid  186  ax1  190  ax2  191  ax3  192  ax5  194  ax7  196  ax8  198  ax9  199  ax10  200  ax11  201  ax13  203  ax14  204  axext  206  axrep  207  axpow  208  axun  209
This theorem was proved from axioms:  ax-cb1 29  ax-refl 39
  Copyright terms: Public domain W3C validator