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 230	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 206  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  1622  nftru  1806  altru  1809  extru  1979  sbtru  2070  vextru  2716  rextru  3077  rabtru  3680  ss2abi  4063  ab0orv  4378  disjprgw  5143  disjprg  5144  reusv2lem5  5400  rabxfr  5416  reuhyp  5418  euotd  5513  mptexgf  7223  elabrex  7241  caovcl  7600  caovass  7606  caovdi  7625  ectocl  8778  fin1a2lem10  10403  riotaneg  12192  zriotaneg  12674  cshwsexaOLD  14774  eflt  16059  efgi0  19587  efgi1  19588  0frgp  19646  iundisj2  25065  pige3ALT  26028  tanord1  26045  tanord  26046  logtayl  26167  iundisj2f  31816  iundisj2fi  32003  ordtconn  32900  tgoldbachgt  33670  nexntru  35284  bj-fal  35442  bj-axd2d  35466  bj-rabtr  35805  bj-rabtrALT  35806  bj-dfid2ALT  35941  bj-finsumval0  36161  wl-impchain-mp-x  36323  wl-impchain-com-1.x  36327  wl-impchain-com-n.m  36332  wl-impchain-a1-x  36336  wl-moteq  36378  ftc1anclem5  36560  lhpexle1  38874  3lexlogpow5ineq2  40915  3lexlogpow2ineq1  40918  3lexlogpow2ineq2  40919  mzpcompact2lem  41479  ifpdfor  42206  ifpim1  42210  ifpnot  42211  ifpid2  42212  ifpim2  42213  uun0.1  43529  uunT1  43531  un10  43539  un01  43540  elabrexg  43718  liminfvalxr  44489  ovn02  45274  rmotru  47479  reutru  47480