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

Theorem tru 1532
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 1531 . 2 (⊤ ↔ (∀𝑥 𝑥 = 𝑥 → ∀𝑥 𝑥 = 𝑥))
31, 2mpbir 232 1
Colors of variables: wff setvar class
Syntax hints:  wi 4  wal 1526   = wceq 1528  wtru 1529
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 208  df-tru 1531
This theorem is referenced by:  dftru2  1533  trut  1534  mptru  1535  tbtru  1536  bitru  1537  trud  1538  truan  1539  fal  1542  truorfal  1566  falortru  1567  trunortruOLD  1578  trunorfalOLD  1580  cadtru  1612  nftru  1796  altru  1799  extru  1971  sbtru  2063  vextru  2803  rabtru  3674  disjprgw  5052  disjprg  5053  reusv2lem5  5293  rabxfr  5309  reuhyp  5311  euotd  5394  elabrex  6993  caovcl  7331  caovass  7337  caovdi  7356  ectocl  8354  fin1a2lem10  9819  riotaneg  11608  zriotaneg  12084  cshwsexa  14174  eflt  15458  efgi0  18775  efgi1  18776  0frgp  18834  iundisj2  24077  pige3ALT  25032  tanord1  25048  tanord  25049  logtayl  25170  iundisj2f  30268  iundisj2fi  30446  ordtconn  31067  tgoldbachgt  31833  nexntru  33649  bj-axd2d  33824  bj-rabtr  34145  bj-rabtrALT  34146  bj-df-v  34241  bj-finsumval0  34455  wl-impchain-mp-x  34610  wl-impchain-com-1.x  34614  wl-impchain-com-n.m  34619  wl-impchain-a1-x  34623  wl-moteq  34636  ftc1anclem5  34852  lhpexle1  37024  mzpcompact2lem  39226  ifpdfor  39708  ifpim1  39712  ifpnot  39713  ifpid2  39714  ifpim2  39715  uun0.1  40989  uunT1  40991  un10  40999  un01  41000  elabrexg  41180  liminfvalxr  41940  ovn02  42727
  Copyright terms: Public domain W3C validator