Theorem tru 1546

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

Syntax hints:   → wi 4  ∀wal 1540   = wceq 1542  ⊤wtru 1543

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 1545

This theorem is referenced by:  dftru2  1547  trut  1548  mptru  1549  tbtru  1550  bitru  1551  trud  1552  truan  1553  fal  1556  truorfal  1580  falortru  1581  cadtru  1622  nftru  1806  altru  1809  extru  1977  sbtru  2073  vextru  2722  rextru  3069  rabtru  3646  ss2abi  4020  disjprg  5096  reusv2lem5  5349  rabxfr  5365  reuhyp  5367  euotd  5469  mptexgf  7178  elabrex  7198  elabrexg  7199  caovcl  7562  caovass  7568  caovdi  7587  ectocl  8732  fin1a2lem10  10331  riotaneg  12133  zriotaneg  12617  eflt  16054  efgi0  19661  efgi1  19662  0frgp  19720  mpomulcn  24826  iundisj2  25518  pige3ALT  26497  tanord1  26514  tanord  26515  logtayl  26637  n0sind  28341  nnsind  28381  iundisj2f  32677  iundisj2fi  32888  ordtconn  34103  tgoldbachgt  34841  nexntru  36620  bj-fal  36793  bj-axd2d  36818  bj-rabtr  37178  bj-rabtrALT  37179  bj-dfid2ALT  37313  bj-finsumval0  37540  wl-impchain-mp-x  37702  wl-impchain-com-1.x  37706  wl-impchain-com-n.m  37711  wl-impchain-a1-x  37715  wl-moteq  37769  ftc1anclem5  37948  lhpexle1  40384  3lexlogpow5ineq2  42425  3lexlogpow2ineq1  42428  3lexlogpow2ineq2  42429  mzpcompact2lem  43108  ifpdfor  43821  ifpim1  43825  ifpnot  43826  ifpid2  43827  ifpim2  43828  uun0.1  45133  uunT1  45135  un10  45143  un01  45144  dfbi1ALTa  45295  simprimi  45296  n0abso  45332  liminfvalxr  46141  ovn02  46926  rmotru  49162  reutru  49163