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  1544  cbv3  1935  disjprg  4035  euotd  4283  reusv2lem5  4555  rabxfr  4572  reuhyp  4578  elabrex  5781  caovcl  6030  caovass  6036  caovdi  6055  ectocl  6743  fin1a2lem10  8051  riotaneg  9745  eflt  12413  efgi0  15045  efgi1  15046  0frgp  15104  iundisj2  18922  pige3  19901  tanord1  19915  tanord  19916  logtayl  20023  iundisj2fi  23379  iundisj2f  23381  allt  24912  nextnt  24916  vutr  25053  trtrst  25119  mzpcompact2lem  26932  uun0.1  28867  un10  28877  un01  28878  cbv3wAUX7  29492  cbv3OLD7  29677  lhpexle1  30819
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