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

Theorem tru 1635
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 1634 . 2 (⊤ ↔ (∀𝑥 𝑥 = 𝑥 → ∀𝑥 𝑥 = 𝑥))
31, 2mpbir 221 1
Colors of variables: wff setvar class
Syntax hints:  wi 4  wal 1629   = wceq 1631  wtru 1632
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 197  df-tru 1634
This theorem is referenced by:  fal  1638  dftru2  1639  trut  1640  trud  1641  tbtru  1642  bitru  1644  a1tru  1648  truan  1649  truorfal  1659  falortru  1660  cadtru  1707  nftru  1878  rabtru  3512  disjprg  4782  reusv2lem5  5002  rabxfr  5018  reuhyp  5024  euotd  5106  elabrex  6644  caovcl  6975  caovass  6981  caovdi  7000  ectocl  7967  fin1a2lem10  9433  riotaneg  11204  zriotaneg  11693  cshwsexa  13779  eflt  15053  efgi0  18340  efgi1  18341  0frgp  18399  iundisj2  23537  pige3  24490  tanord1  24504  tanord  24505  logtayl  24627  iundisj2f  29741  iundisj2fi  29896  ordtconn  30311  tgoldbachgt  31081  allt  32737  nextnt  32741  bj-axd2d  32914  bj-extru  32991  bj-rabtr  33258  bj-rabtrALT  33259  bj-rabtrALTALT  33260  bj-df-v  33347  bj-finsumval0  33484  wl-impchain-mp-x  33608  wl-impchain-com-1.x  33612  wl-impchain-com-n.m  33617  wl-impchain-a1-x  33621  ftc1anclem5  33821  lhpexle1  35816  mzpcompact2lem  37840  ifpdfor  38335  ifpim1  38339  ifpnot  38340  ifpid2  38341  ifpim2  38342  uun0.1  39530  uunT1  39532  un10  39540  un01  39541  elabrexg  39728  liminfvalxr  40533  ovn02  41302
  Copyright terms: Public domain W3C validator