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

Theorem tru 1485
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 1484 . 2 (⊤ ↔ (∀𝑥 𝑥 = 𝑥 → ∀𝑥 𝑥 = 𝑥))
31, 2mpbir 221 1
Colors of variables: wff setvar class
Syntax hints:  wi 4  wal 1479   = wceq 1481  wtru 1482
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 1484
This theorem is referenced by:  fal  1488  dftru2  1489  trut  1490  trud  1491  tbtru  1492  bitru  1494  a1tru  1498  truan  1499  truorfal  1509  falortru  1510  cadtru  1557  nftru  1728  rabtru  3355  disjprg  4639  reusv2lem5  4864  rabxfr  4881  reuhyp  4887  euotd  4965  elabrex  6486  caovcl  6813  caovass  6819  caovdi  6838  ectocl  7800  fin1a2lem10  9216  riotaneg  10987  zriotaneg  11476  cshwsexa  13551  eflt  14828  efgi0  18114  efgi1  18115  0frgp  18173  iundisj2  23298  pige3  24250  tanord1  24264  tanord  24265  logtayl  24387  iundisj2f  29375  iundisj2fi  29530  ordtconn  29945  tgoldbachgt  30715  allt  32375  nextnt  32379  bj-axd2d  32552  bj-extru  32629  bj-rabtr  32901  bj-rabtrALT  32902  bj-rabtrALTALT  32903  bj-df-v  32991  bj-finsumval0  33118  wl-impchain-mp-x  33240  wl-impchain-com-1.x  33244  wl-impchain-com-n.m  33249  wl-impchain-a1-x  33253  ftc1anclem5  33460  lhpexle1  35113  mzpcompact2lem  37133  ifpdfor  37628  ifpim1  37632  ifpnot  37633  ifpid2  37634  ifpim2  37635  uun0.1  38825  uunT1  38827  un10  38835  un01  38836  elabrexg  39026  liminfvalxr  39809  ovn02  40545
  Copyright terms: Public domain W3C validator