Theorem tru 1540

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

Syntax hints:   → wi 4  ∀wal 1534   = wceq 1536  ⊤wtru 1537

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 1539

This theorem is referenced by:  dftru2  1541  trut  1542  mptru  1543  tbtru  1544  bitru  1545  trud  1546  truan  1547  fal  1550  truorfal  1574  falortru  1575  cadtru  1616  nftru  1800  altru  1803  extru  1972  sbtru  2064  vextru  2718  rextru  3074  rabtru  3691  ss2abi  4076  ab0orv  4388  disjprg  5143  reusv2lem5  5407  rabxfr  5423  reuhyp  5425  euotd  5522  mptexgf  7241  elabrex  7261  elabrexg  7262  caovcl  7626  caovass  7632  caovdi  7651  ectocl  8823  fin1a2lem10  10446  riotaneg  12244  zriotaneg  12728  cshwsexaOLD  14859  eflt  16149  efgi0  19752  efgi1  19753  0frgp  19811  mpomulcn  24904  iundisj2  25597  pige3ALT  26576  tanord1  26593  tanord  26594  logtayl  26716  n0sind  28351  nnsind  28377  iundisj2f  32609  iundisj2fi  32804  ordtconn  33885  tgoldbachgt  34656  nexntru  36386  bj-fal  36552  bj-axd2d  36575  bj-rabtr  36912  bj-rabtrALT  36913  bj-dfid2ALT  37047  bj-finsumval0  37267  wl-impchain-mp-x  37429  wl-impchain-com-1.x  37433  wl-impchain-com-n.m  37438  wl-impchain-a1-x  37442  wl-moteq  37494  ftc1anclem5  37683  lhpexle1  39990  3lexlogpow5ineq2  42036  3lexlogpow2ineq1  42039  3lexlogpow2ineq2  42040  mzpcompact2lem  42738  ifpdfor  43454  ifpim1  43458  ifpnot  43459  ifpid2  43460  ifpim2  43461  uun0.1  44775  uunT1  44777  un10  44785  un01  44786  liminfvalxr  45738  ovn02  46523  rmotru  48651  reutru  48652