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 231	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 207  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  1621  nftru  1805  altru  1808  extru  1976  sbtru  2072  vextru  2719  rextru  3065  rabtru  3642  ss2abi  4016  disjprg  5092  reusv2lem5  5345  rabxfr  5361  reuhyp  5363  euotd  5459  mptexgf  7166  elabrex  7186  elabrexg  7187  caovcl  7550  caovass  7556  caovdi  7575  ectocl  8718  fin1a2lem10  10317  riotaneg  12119  zriotaneg  12603  eflt  16040  efgi0  19647  efgi1  19648  0frgp  19706  mpomulcn  24812  iundisj2  25504  pige3ALT  26483  tanord1  26500  tanord  26501  logtayl  26623  n0sind  28293  nnsind  28331  iundisj2f  32614  iundisj2fi  32826  ordtconn  34031  tgoldbachgt  34769  nexntru  36547  bj-fal  36713  bj-axd2d  36736  bj-rabtr  37074  bj-rabtrALT  37075  bj-dfid2ALT  37209  bj-finsumval0  37429  wl-impchain-mp-x  37591  wl-impchain-com-1.x  37595  wl-impchain-com-n.m  37600  wl-impchain-a1-x  37604  wl-moteq  37658  ftc1anclem5  37837  lhpexle1  40207  3lexlogpow5ineq2  42248  3lexlogpow2ineq1  42251  3lexlogpow2ineq2  42252  mzpcompact2lem  42935  ifpdfor  43648  ifpim1  43652  ifpnot  43653  ifpid2  43654  ifpim2  43655  uun0.1  44960  uunT1  44962  un10  44970  un01  44971  dfbi1ALTa  45122  simprimi  45123  n0abso  45159  liminfvalxr  45969  ovn02  46754  rmotru  48990  reutru  48991