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

Theorem tru 1657
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 1656 . 2 (⊤ ↔ (∀𝑥 𝑥 = 𝑥 → ∀𝑥 𝑥 = 𝑥))
31, 2mpbir 222 1
Colors of variables: wff setvar class
Syntax hints:  wi 4  wal 1650   = wceq 1652  wtru 1653
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 198  df-tru 1656
This theorem is referenced by:  dftru2  1658  trut  1659  mptru  1660  tbtru  1661  bitru  1662  trud  1663  truan  1664  fal  1667  truorfal  1691  falortru  1692  cadtru  1729  nftru  1899  altru  1902  rabtru  3518  disjprg  4807  reusv2lem5  5039  rabxfr  5055  reuhyp  5061  euotd  5136  elabrex  6695  caovcl  7028  caovass  7034  caovdi  7053  ectocl  8020  fin1a2lem10  9486  riotaneg  11258  zriotaneg  11741  cshwsexa  13856  eflt  15132  efgi0  18400  efgi1  18401  0frgp  18461  iundisj2  23610  pige3  24564  tanord1  24578  tanord  24579  logtayl  24700  iundisj2f  29854  iundisj2fi  30008  ordtconn  30421  tgoldbachgt  31195  nexntru  32846  bj-axd2d  33016  bj-extru  33093  bj-rabtr  33357  bj-rabtrALT  33358  bj-rabtrALTALT  33359  bj-df-v  33446  bj-finsumval0  33584  wl-impchain-mp-x  33707  wl-impchain-com-1.x  33711  wl-impchain-com-n.m  33716  wl-impchain-a1-x  33720  ftc1anclem5  33915  lhpexle1  35967  mzpcompact2lem  37995  ifpdfor  38488  ifpim1  38492  ifpnot  38493  ifpid2  38494  ifpim2  38495  uun0.1  39669  uunT1  39671  un10  39679  un01  39680  elabrexg  39861  liminfvalxr  40656  ovn02  41425
  Copyright terms: Public domain W3C validator