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  36382  bj-fal  36548  bj-axd2d  36571  bj-rabtr  36908  bj-rabtrALT  36909  bj-dfid2ALT  37043  bj-finsumval0  37263  wl-impchain-mp-x  37425  wl-impchain-com-1.x  37429  wl-impchain-com-n.m  37434  wl-impchain-a1-x  37438  wl-moteq  37492  ftc1anclem5  37681  lhpexle1  39991  3lexlogpow5ineq2  42032  3lexlogpow2ineq1  42035  3lexlogpow2ineq2  42036  mzpcompact2lem  42728  ifpdfor  43442  ifpim1  43446  ifpnot  43447  ifpid2  43448  ifpim2  43449  uun0.1  44755  uunT1  44757  un10  44765  un01  44766  dfbi1ALTa  44917  simprimi  44918  n0abso  44954  liminfvalxr  45768  ovn02  46553  rmotru  48791  reutru  48792