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

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

Proof of Theorem tru
StepHypRef Expression
1 biid 227 . 2  |-  ( ph  <->  ph )
2 df-tru 1310 . 2  |-  (  T.  <->  (
ph 
<-> 
ph ) )
31, 2mpbir 200 1  |-  T.
Colors of variables: wff set class
Syntax hints:    <-> wb 176    T. wtru 1307
This theorem is referenced by:  fal  1313  trud  1314  tbtru  1315  bitru  1317  a1tru  1321  truorfal  1331  falortru  1332  truimfal  1335  cadtru  1391  nftru  1541  cbv3  1922  disjprg  4019  euotd  4267  reusv2lem5  4539  rabxfr  4556  reuhyp  4562  elabrex  5765  caovcl  6014  caovass  6020  caovdi  6039  ectocl  6727  fin1a2lem10  8035  riotaneg  9729  eflt  12397  efgi0  15029  efgi1  15030  0frgp  15088  iundisj2  18906  pige3  19885  tanord1  19899  tanord  19900  logtayl  20007  iundisj2fi  23364  iundisj2f  23366  allt  24840  nextnt  24844  vutr  24950  trtrst  25016  mzpcompact2lem  26829  uun0.1  28553  un10  28563  un01  28564  lhpexle1  30197
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 177  df-tru 1310
  Copyright terms: Public domain W3C validator