MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  tru Structured version   Unicode version

Theorem tru 1387
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 22 . 2  |-  ( A. x  x  =  x  ->  A. x  x  =  x )
2 df-tru 1386 . 2  |-  ( T.  <-> 
( A. x  x  =  x  ->  A. x  x  =  x )
)
31, 2mpbir 209 1  |- T.
Colors of variables: wff setvar class
Syntax hints:    -> wi 4   A.wal 1381    = wceq 1383   T. wtru 1384
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8
This theorem depends on definitions:  df-bi 185  df-tru 1386
This theorem is referenced by:  fal  1390  dftru2  1391  trud  1392  tbtru  1393  bitru  1395  a1tru  1399  truan  1400  truorfal  1412  falortru  1413  truimfal  1416  cadtru  1456  nftru  1613  disjprg  4433  reusv2lem5  4642  rabxfr  4659  reuhyp  4665  euotd  4738  elabrex  6140  caovcl  6454  caovass  6460  caovdi  6479  ectocl  7381  fin1a2lem10  8792  riotaneg  10525  zriotaneg  10984  cshwsexa  12774  eflt  13834  efgi0  16717  efgi1  16718  0frgp  16776  iundisj2  21937  pige3  22888  tanord1  22902  tanord  22903  logtayl  23019  iundisj2f  27427  iundisj2fi  27580  ordtcon  27885  allt  29842  nextnt  29846  wl-impchain-mp-x  29932  wl-impchain-com-1.x  29936  wl-impchain-com-n.m  29941  ftc1anclem5  30070  mzpcompact2lem  30660  elabrexg  31384  etransclem46  32017  uun0.1  33443  uunT1  33445  un10  33453  un01  33454  bj-trut  34054  bj-axd2d  34064  bj-rabtr  34380  bj-rabtrALT  34381  bj-df-v  34466  bj-finsumval0  34538  lhpexle1  35607
  Copyright terms: Public domain W3C validator