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  2715  rextru  3061  rabtru  3659  ss2abi  4033  ab0orv  4349  disjprg  5106  reusv2lem5  5360  rabxfr  5376  reuhyp  5378  euotd  5476  mptexgf  7199  elabrex  7219  elabrexg  7220  caovcl  7586  caovass  7592  caovdi  7611  ectocl  8759  fin1a2lem10  10369  riotaneg  12169  zriotaneg  12654  cshwsexaOLD  14797  eflt  16092  efgi0  19657  efgi1  19658  0frgp  19716  mpomulcn  24765  iundisj2  25457  pige3ALT  26436  tanord1  26453  tanord  26454  logtayl  26576  n0sind  28232  nnsind  28269  iundisj2f  32526  iundisj2fi  32727  ordtconn  33922  tgoldbachgt  34661  nexntru  36399  bj-fal  36565  bj-axd2d  36588  bj-rabtr  36925  bj-rabtrALT  36926  bj-dfid2ALT  37060  bj-finsumval0  37280  wl-impchain-mp-x  37442  wl-impchain-com-1.x  37446  wl-impchain-com-n.m  37451  wl-impchain-a1-x  37455  wl-moteq  37509  ftc1anclem5  37698  lhpexle1  40009  3lexlogpow5ineq2  42050  3lexlogpow2ineq1  42053  3lexlogpow2ineq2  42054  mzpcompact2lem  42746  ifpdfor  43461  ifpim1  43465  ifpnot  43466  ifpid2  43467  ifpim2  43468  uun0.1  44774  uunT1  44776  un10  44784  un01  44785  dfbi1ALTa  44936  simprimi  44937  n0abso  44973  liminfvalxr  45788  ovn02  46573  rmotru  48795  reutru  48796