Theorem wtru 43

Description: Truth type. (Contributed by Mario Carneiro, 10-Oct-2014.)

Assertion

Ref	Expression
wtru	⊢ ⊤:∗

Proof of Theorem wtru

Step	Hyp	Ref	Expression
1		weq 41	. . 3 ⊢ = :(∗ → (∗ → ∗))
2	1	ax-refl 42	. 2 ⊢ ⊤⊧(( = = ) = )
3	2	ax-cb1 29	1 ⊢ ⊤:∗

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