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

Theorem wtru 43
Description: Truth type. (Contributed by Mario Carneiro, 10-Oct-2014.)
Assertion
Ref Expression
wtru ⊤:∗

Proof of Theorem wtru
StepHypRef Expression
1 weq 41 . . 3 = :(∗ → (∗ → ∗))
21ax-refl 42 . 2 ⊤⊧(( = = ) = )
32ax-cb1 29 1 ⊤:∗
Colors of variables: type var term
Syntax hints:  ht 2  hb 3  kc 5   = ke 7  kt 8  wffMMJ2t 12
This theorem was proved from axioms:  ax-cb1 29  ax-weq 40  ax-refl 42
This theorem is referenced by:  tru  44  dedi  85  eqtru  86  hbth  109  hbov  111  ovl  117  wal  134  wan  136  alval  142  anval  148  alrimiv  151  dfan2  154  hbct  155  olc  164  orc  165  alrimi  182  exlimd  183  alnex  186  exnal1  187  dfex2  198  exmid  199  ax1  203  ax2  204  ax3  205  ax5  207  ax7  209  ax8  211  ax9  212  ax10  213  ax11  214  ax13  216  ax14  217  axext  219  axrep  220  axpow  221  axun  222
  Copyright terms: Public domain W3C validator