Theorem tru 1574

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 23	. 2 ⊢ (∀𝑥 𝑥 = 𝑥 → ∀𝑥 𝑥 = 𝑥)
2		df-tru 1573	. 2 ⊢ (⊤ ↔ (∀𝑥 𝑥 = 𝑥 → ∀𝑥 𝑥 = 𝑥))
3	1, 2	mpbir 234	1 ⊢ ⊤

This proof depends on syntax axioms:   → wi 4  ∀wal 1568   = wceq 1570  ⊤wtru 1571

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-tru 1573

This theorem is used by:  dftru2  1575  trut  1576  mptru  1577  tbtru  1578  bitru  1579  trud  1580  truan  1581  fal  1584  truorfal  1608  falortru  1609  cadtru  1653  nftru  1837  altru  1840  extru  2010  sbtru  2106  vextru  2748  rextru  3097  rabtru  3646  disjprg  5104  reusv2lem5  5371  rabxfr  5387  reuhyp  5389  euotd  5493  mptexgf  7259  elabrex  7277  elabrexg  7278  caovcl  7647  caovass  7653  caovdi  7672  ectocl  8842  fin1a2lem10  10526  riotaneg  12336  zriotaneg  12852  eflt  16329  efgi0  19985  efgi1  19986  0frgp  20044  mpomulcn  25243  iundisj2  25925  pige3ALT  26905  tanord1  26922  tanord  26923  logtayl  27045  n0sind  28776  nnsind  28816  iundisj2f  33282  iundisj2fi  33485  ordtconn  34668  tgoldbachgt  35403  nexntru  37407  bj-fal  37653  bj-axd2d  37678  bj-rabtr  38058  bj-rabtrALT  38059  bj-dfid2ALT  38250  bj-finsumval0  38474  wl-impchain-mp-x  38638  wl-impchain-com-1.x  38642  wl-impchain-com-n.m  38647  wl-impchain-a1-x  38651  wl-moteq  38714  ftc1anclem5  38883  lhpexle1  41331  3lexlogpow5ineq2  43371  3lexlogpow2ineq1  43374  3lexlogpow2ineq2  43375  mzpcompact2lem  44028  ifpdfor  44727  ifpim1  44731  ifpnot  44732  ifpid2  44733  ifpim2  44734  uun0.1  46020  uunT1  46022  un10  46030  un01  46031  dfbi1ALTa  46193  simprimi  46194  n0abso  46230  liminfvalxr  47066  ovn02  47851  rmotru  50244  reutru  50245