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  2067  vextru  2721  rextru  3077  rabtru  3689  ss2abi  4067  ab0orv  4383  disjprg  5139  reusv2lem5  5402  rabxfr  5418  reuhyp  5420  euotd  5518  mptexgf  7242  elabrex  7262  elabrexg  7263  caovcl  7627  caovass  7633  caovdi  7652  ectocl  8825  fin1a2lem10  10449  riotaneg  12247  zriotaneg  12731  cshwsexaOLD  14863  eflt  16153  efgi0  19738  efgi1  19739  0frgp  19797  mpomulcn  24891  iundisj2  25584  pige3ALT  26562  tanord1  26579  tanord  26580  logtayl  26702  n0sind  28337  nnsind  28363  iundisj2f  32603  iundisj2fi  32799  ordtconn  33924  tgoldbachgt  34678  nexntru  36405  bj-fal  36571  bj-axd2d  36594  bj-rabtr  36931  bj-rabtrALT  36932  bj-dfid2ALT  37066  bj-finsumval0  37286  wl-impchain-mp-x  37448  wl-impchain-com-1.x  37452  wl-impchain-com-n.m  37457  wl-impchain-a1-x  37461  wl-moteq  37515  ftc1anclem5  37704  lhpexle1  40010  3lexlogpow5ineq2  42056  3lexlogpow2ineq1  42059  3lexlogpow2ineq2  42060  mzpcompact2lem  42762  ifpdfor  43478  ifpim1  43482  ifpnot  43483  ifpid2  43484  ifpim2  43485  uun0.1  44798  uunT1  44800  un10  44808  un01  44809  dfbi1ALTa  44960  simprimi  44961  n0abso  44993  liminfvalxr  45798  ovn02  46583  rmotru  48723  reutru  48724