ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  tru Unicode version

Theorem tru 1318
Description: The truth value T. is provable. (Contributed by Anthony Hart, 13-Oct-2010.)
Assertion
Ref Expression
tru  |- T.

Proof of Theorem tru
StepHypRef Expression
1 id 19 . 2  |-  ( A. x  x  =  x  ->  A. x  x  =  x )
2 df-tru 1317 . 2  |-  ( T.  <-> 
( A. x  x  =  x  ->  A. x  x  =  x )
)
31, 2mpbir 145 1  |- T.
Colors of variables: wff set class
Syntax hints:    -> wi 4   A.wal 1312    = wceq 1314   T. wtru 1315
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107
This theorem depends on definitions:  df-bi 116  df-tru 1317
This theorem is referenced by:  fal  1321  dftru2  1322  mptru  1323  tbtru  1324  bitru  1326  a1tru  1330  truan  1331  truorfal  1367  falortru  1368  truimfal  1371  nftru  1425  euotd  4144  rabxfr  4359  reuhyp  4361  elabrex  5625  caovcl  5891  caovass  5897  caovdi  5916  ectocl  6462  reef11  11305  bj-sbimeh  12790  bdtru  12841  bj-nn0suc0  12959
  Copyright terms: Public domain W3C validator