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

Theorem tru 1527
 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 1526 . 2 (⊤ ↔ (∀𝑥 𝑥 = 𝑥 → ∀𝑥 𝑥 = 𝑥))
31, 2mpbir 221 1
 Colors of variables: wff setvar class Syntax hints:   → wi 4  ∀wal 1521   = wceq 1523  ⊤wtru 1524 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 1526 This theorem is referenced by:  fal  1530  dftru2  1531  trut  1532  trud  1533  tbtru  1534  bitru  1536  a1tru  1540  truan  1541  truorfal  1551  falortru  1552  cadtru  1599  nftru  1770  rabtru  3393  disjprg  4680  reusv2lem5  4903  rabxfr  4920  reuhyp  4926  euotd  5004  elabrex  6541  caovcl  6870  caovass  6876  caovdi  6895  ectocl  7858  fin1a2lem10  9269  riotaneg  11040  zriotaneg  11529  cshwsexa  13616  eflt  14891  efgi0  18179  efgi1  18180  0frgp  18238  iundisj2  23363  pige3  24314  tanord1  24328  tanord  24329  logtayl  24451  iundisj2f  29529  iundisj2fi  29684  ordtconn  30099  tgoldbachgt  30869  allt  32525  nextnt  32529  bj-axd2d  32702  bj-extru  32779  bj-rabtr  33051  bj-rabtrALT  33052  bj-rabtrALTALT  33053  bj-df-v  33141  bj-finsumval0  33277  wl-impchain-mp-x  33399  wl-impchain-com-1.x  33403  wl-impchain-com-n.m  33408  wl-impchain-a1-x  33412  ftc1anclem5  33619  lhpexle1  35612  mzpcompact2lem  37631  ifpdfor  38126  ifpim1  38130  ifpnot  38131  ifpid2  38132  ifpim2  38133  uun0.1  39322  uunT1  39324  un10  39332  un01  39333  elabrexg  39520  liminfvalxr  40333  ovn02  41103
 Copyright terms: Public domain W3C validator