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

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

Proof of Theorem tru
StepHypRef Expression
1 biid 228 . 2  |-  ( ph  <->  ph )
2 df-tru 1328 . 2  |-  (  T.  <->  (
ph 
<-> 
ph ) )
31, 2mpbir 201 1  |-  T.
Colors of variables: wff set class
Syntax hints:    <-> wb 177    T. wtru 1325
This theorem is referenced by:  fal  1331  trud  1332  tbtru  1333  bitru  1335  a1tru  1339  truorfal  1350  falortru  1351  truimfal  1354  cadtru  1410  nftru  1563  cbv3OLD  1978  disjprg  4200  euotd  4449  reusv2lem5  4720  rabxfr  4737  reuhyp  4743  elabrex  5977  caovcl  6233  caovass  6239  caovdi  6258  ectocl  6964  fin1a2lem10  8281  riotaneg  9975  eflt  12710  efgi0  15344  efgi1  15345  0frgp  15403  iundisj2  19435  pige3  20417  tanord1  20431  tanord  20432  logtayl  20543  iundisj2f  24022  iundisj2fi  24145  allt  26143  nextnt  26147  ftc1anclem5  26274  mzpcompact2lem  26799  cshwsexa  28254  uun0.1  28827  un10  28837  un01  28838  cbv3wAUX7  29454  cbv3OLD7  29660  lhpexle1  30742
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
This theorem depends on definitions:  df-bi 178  df-tru 1328
  Copyright terms: Public domain W3C validator