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 ⊢ ⊤

Syntax hints:   → wi 4  ∀wal 1568   = wceq 1570  ⊤wtru 1571

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 210  df-tru 1573

This theorem is referenced by:  dftru2  1575  trut  1576  mptru  1577  tbtru  1578  bitru  1579  trud  1580  truan  1581  fal  1584  truorfal  1608  falortru  1609  cadtru  1650  nftru  1834  altru  1837  extru  2005  sbtru  2101  vextru  2748  rextru  3096  rabtru  3648  disjprg  5105  reusv2lem5  5373  rabxfr  5389  reuhyp  5391  euotd  5496  mptexgf  7220  elabrex  7240  elabrexg  7241  caovcl  7604  caovass  7610  caovdi  7629  ectocl  8777  fin1a2lem10  10388  riotaneg  12189  zriotaneg  12704  eflt  16168  efgi0  19785  efgi1  19786  0frgp  19844  mpomulcn  25026  iundisj2  25708  pige3ALT  26685  tanord1  26702  tanord  26703  logtayl  26825  n0sind  28526  nnsind  28566  iundisj2f  32935  iundisj2fi  33142  ordtconn  34315  tgoldbachgt  35050  nexntru  36935  bj-fal  37181  bj-axd2d  37206  bj-rabtr  37586  bj-rabtrALT  37587  bj-dfid2ALT  37721  bj-finsumval0  37949  wl-impchain-mp-x  38113  wl-impchain-com-1.x  38117  wl-impchain-com-n.m  38122  wl-impchain-a1-x  38126  wl-moteq  38189  ftc1anclem5  38368  lhpexle1  40802  3lexlogpow5ineq2  42842  3lexlogpow2ineq1  42845  3lexlogpow2ineq2  42846  mzpcompact2lem  43502  ifpdfor  44211  ifpim1  44215  ifpnot  44216  ifpid2  44217  ifpim2  44218  uun0.1  45506  uunT1  45508  un10  45516  un01  45517  dfbi1ALTa  45668  simprimi  45669  n0abso  45705  liminfvalxr  46517  ovn02  47302  rmotru  49601  reutru  49602