Theorem tru 1545

Description: The truth value ⊤ is provable. (Contributed by Anthony Hart, 13-Oct-2010.)

Assertion

Ref	Expression
tru	⊢ ⊤

Proof of Theorem tru

Step	Hyp	Ref	Expression
1		id 22	. 2 ⊢ (∀𝑥 𝑥 = 𝑥 → ∀𝑥 𝑥 = 𝑥)
2		df-tru 1544	. 2 ⊢ (⊤ ↔ (∀𝑥 𝑥 = 𝑥 → ∀𝑥 𝑥 = 𝑥))
3	1, 2	mpbir 231	1 ⊢ ⊤

Syntax hints:   → wi 4  ∀wal 1539   = wceq 1541  ⊤wtru 1542

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 207  df-tru 1544

This theorem is referenced by:  dftru2  1546  trut  1547  mptru  1548  tbtru  1549  bitru  1550  trud  1551  truan  1552  fal  1555  truorfal  1579  falortru  1580  cadtru  1621  nftru  1805  altru  1808  extru  1976  sbtru  2070  vextru  2716  rextru  3063  rabtru  3640  ss2abi  4013  disjprg  5085  reusv2lem5  5338  rabxfr  5354  reuhyp  5356  euotd  5451  mptexgf  7156  elabrex  7176  elabrexg  7177  caovcl  7540  caovass  7546  caovdi  7565  ectocl  8707  fin1a2lem10  10300  riotaneg  12101  zriotaneg  12586  eflt  16026  efgi0  19632  efgi1  19633  0frgp  19691  mpomulcn  24785  iundisj2  25477  pige3ALT  26456  tanord1  26473  tanord  26474  logtayl  26596  n0sind  28261  nnsind  28298  iundisj2f  32570  iundisj2fi  32779  ordtconn  33938  tgoldbachgt  34676  nexntru  36448  bj-fal  36614  bj-axd2d  36637  bj-rabtr  36974  bj-rabtrALT  36975  bj-dfid2ALT  37109  bj-finsumval0  37329  wl-impchain-mp-x  37491  wl-impchain-com-1.x  37495  wl-impchain-com-n.m  37500  wl-impchain-a1-x  37504  wl-moteq  37558  ftc1anclem5  37747  lhpexle1  40117  3lexlogpow5ineq2  42158  3lexlogpow2ineq1  42161  3lexlogpow2ineq2  42162  mzpcompact2lem  42854  ifpdfor  43568  ifpim1  43572  ifpnot  43573  ifpid2  43574  ifpim2  43575  uun0.1  44880  uunT1  44882  un10  44890  un01  44891  dfbi1ALTa  45042  simprimi  45043  n0abso  45079  liminfvalxr  45891  ovn02  46676  rmotru  48913  reutru  48914