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

Theorem tru 1545
Description: The truth value is provable. (Contributed by Anthony Hart, 13-Oct-2010.)
Assertion
Ref Expression
tru

Proof of Theorem tru
StepHypRef Expression
1 id 22 . 2 (∀𝑥 𝑥 = 𝑥 → ∀𝑥 𝑥 = 𝑥)
2 df-tru 1544 . 2 (⊤ ↔ (∀𝑥 𝑥 = 𝑥 → ∀𝑥 𝑥 = 𝑥))
31, 2mpbir 230 1
Colors of variables: wff setvar class
Syntax hints:  wi 4  wal 1539   = wceq 1541  wtru 1542
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 206  df-tru 1544
This theorem is referenced by:  dftru2  1546  trut  1547  mptru  1548  tbtru  1549  bitru  1550  trud  1551  truan  1552  fal  1555  truorfal  1579  falortru  1580  cadtru  1622  nftru  1806  altru  1809  extru  1979  sbtru  2070  vextru  2721  rextru  3078  rabtru  3640  ss2abi  4021  ab0orv  4336  disjprgw  5098  disjprg  5099  reusv2lem5  5355  rabxfr  5371  reuhyp  5373  euotd  5468  mptexgf  7168  elabrex  7186  caovcl  7542  caovass  7548  caovdi  7567  ectocl  8682  fin1a2lem10  10303  riotaneg  12092  zriotaneg  12574  cshwsexaOLD  14671  eflt  15959  efgi0  19461  efgi1  19462  0frgp  19520  iundisj2  24865  pige3ALT  25828  tanord1  25845  tanord  25846  logtayl  25967  iundisj2f  31337  iundisj2fi  31526  ordtconn  32318  tgoldbachgt  33088  nexntru  34814  bj-fal  34972  bj-axd2d  34996  bj-rabtr  35338  bj-rabtrALT  35339  bj-dfid2ALT  35474  bj-finsumval0  35694  wl-impchain-mp-x  35856  wl-impchain-com-1.x  35860  wl-impchain-com-n.m  35865  wl-impchain-a1-x  35869  wl-moteq  35911  ftc1anclem5  36093  lhpexle1  38409  3lexlogpow5ineq2  40450  3lexlogpow2ineq1  40453  3lexlogpow2ineq2  40454  mzpcompact2lem  40983  ifpdfor  41648  ifpim1  41652  ifpnot  41653  ifpid2  41654  ifpim2  41655  uun0.1  42971  uunT1  42973  un10  42981  un01  42982  elabrexg  43160  liminfvalxr  43925  ovn02  44710  rmotru  46790  reutru  46791
  Copyright terms: Public domain W3C validator