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

Theorem tru 1293
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 1292 . 2  |-  ( T.  <-> 
( A. x  x  =  x  ->  A. x  x  =  x )
)
31, 2mpbir 144 1  |- T.
Colors of variables: wff set class
Syntax hints:    -> wi 4   A.wal 1287    = wceq 1289   T. wtru 1290
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106
This theorem depends on definitions:  df-bi 115  df-tru 1292
This theorem is referenced by:  fal  1296  dftru2  1297  mptru  1298  tbtru  1299  bitru  1301  a1tru  1305  truan  1306  truorfal  1342  falortru  1343  truimfal  1346  nftru  1400  euotd  4081  rabxfr  4292  reuhyp  4294  elabrex  5537  caovcl  5799  caovass  5805  caovdi  5824  ectocl  6359  reef11  10990  bj-sbimeh  11673  bdtru  11723  bj-nn0suc0  11845
  Copyright terms: Public domain W3C validator