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  32741  ordtconn  33898  tgoldbachgt  34637  nexntru  36388  bj-fal  36554  bj-axd2d  36577  bj-rabtr  36914  bj-rabtrALT  36915  bj-dfid2ALT  37049  bj-finsumval0  37269  wl-impchain-mp-x  37431  wl-impchain-com-1.x  37435  wl-impchain-com-n.m  37440  wl-impchain-a1-x  37444  wl-moteq  37498  ftc1anclem5  37687  lhpexle1  39997  3lexlogpow5ineq2  42038  3lexlogpow2ineq1  42041  3lexlogpow2ineq2  42042  mzpcompact2lem  42734  ifpdfor  43448  ifpim1  43452  ifpnot  43453  ifpid2  43454  ifpim2  43455  uun0.1  44761  uunT1  44763  un10  44771  un01  44772  dfbi1ALTa  44923  simprimi  44924  n0abso  44960  liminfvalxr  45774  ovn02  46559  rmotru  48797  reutru  48798