Theorem tru 1544

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 1543	. 2 ⊢ (⊤ ↔ (∀𝑥 𝑥 = 𝑥 → ∀𝑥 𝑥 = 𝑥))
3	1, 2	mpbir 231	1 ⊢ ⊤

Syntax hints:   → wi 4  ∀wal 1538   = wceq 1540  ⊤wtru 1541

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 1543

This theorem is referenced by:  dftru2  1545  trut  1546  mptru  1547  tbtru  1548  bitru  1549  trud  1550  truan  1551  fal  1554  truorfal  1578  falortru  1579  cadtru  1620  nftru  1804  altru  1807  extru  1975  sbtru  2068  vextru  2714  rextru  3060  rabtru  3645  ss2abi  4019  ab0orv  4334  disjprg  5088  reusv2lem5  5341  rabxfr  5357  reuhyp  5359  euotd  5456  mptexgf  7158  elabrex  7178  elabrexg  7179  caovcl  7543  caovass  7549  caovdi  7568  ectocl  8710  fin1a2lem10  10303  riotaneg  12104  zriotaneg  12589  cshwsexaOLD  14731  eflt  16026  efgi0  19599  efgi1  19600  0frgp  19658  mpomulcn  24756  iundisj2  25448  pige3ALT  26427  tanord1  26444  tanord  26445  logtayl  26567  n0sind  28230  nnsind  28267  iundisj2f  32534  iundisj2fi  32740  ordtconn  33892  tgoldbachgt  34631  nexntru  36378  bj-fal  36544  bj-axd2d  36567  bj-rabtr  36904  bj-rabtrALT  36905  bj-dfid2ALT  37039  bj-finsumval0  37259  wl-impchain-mp-x  37421  wl-impchain-com-1.x  37425  wl-impchain-com-n.m  37430  wl-impchain-a1-x  37434  wl-moteq  37488  ftc1anclem5  37677  lhpexle1  39987  3lexlogpow5ineq2  42028  3lexlogpow2ineq1  42031  3lexlogpow2ineq2  42032  mzpcompact2lem  42724  ifpdfor  43438  ifpim1  43442  ifpnot  43443  ifpid2  43444  ifpim2  43445  uun0.1  44751  uunT1  44753  un10  44761  un01  44762  dfbi1ALTa  44913  simprimi  44914  n0abso  44950  liminfvalxr  45764  ovn02  46549  rmotru  48787  reutru  48788