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

Theorem tru 1289
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 1288 . 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 1283    = wceq 1285   T. wtru 1286
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 1288
This theorem is referenced by:  fal  1292  dftru2  1293  trud  1294  tbtru  1295  bitru  1297  a1tru  1301  truan  1302  truorfal  1338  falortru  1339  truimfal  1342  nftru  1396  euotd  4017  rabxfr  4228  reuhyp  4230  elabrex  5429  caovcl  5686  caovass  5692  caovdi  5711  ectocl  6239  bj-sbimeh  10734  bdtru  10781  bj-nn0suc0  10903
  Copyright terms: Public domain W3C validator