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  2008  sbtru  2104  vextru  2746  rextru  3094  rabtru  3643  disjprg  5099  reusv2lem5  5364  rabxfr  5380  reuhyp  5382  euotd  5486  mptexgf  7228  elabrex  7246  elabrexg  7247  caovcl  7615  caovass  7621  caovdi  7640  ectocl  8804  fin1a2lem10  10487  riotaneg  12296  zriotaneg  12812  eflt  16285  efgi0  19934  efgi1  19935  0frgp  19993  mpomulcn  25188  iundisj2  25870  pige3ALT  26848  tanord1  26865  tanord  26866  logtayl  26988  n0sind  28719  nnsind  28759  iundisj2f  33184  iundisj2fi  33389  ordtconn  34557  tgoldbachgt  35292  nexntru  37192  bj-fal  37438  bj-axd2d  37463  bj-rabtr  37843  bj-rabtrALT  37844  bj-dfid2ALT  37980  bj-finsumval0  38206  wl-impchain-mp-x  38370  wl-impchain-com-1.x  38374  wl-impchain-com-n.m  38379  wl-impchain-a1-x  38383  wl-moteq  38446  ftc1anclem5  38615  lhpexle1  41065  3lexlogpow5ineq2  43105  3lexlogpow2ineq1  43108  3lexlogpow2ineq2  43109  mzpcompact2lem  43761  ifpdfor  44465  ifpim1  44469  ifpnot  44470  ifpid2  44471  ifpim2  44472  uun0.1  45759  uunT1  45761  un10  45769  un01  45770  dfbi1ALTa  45928  simprimi  45929  n0abso  45965  liminfvalxr  46792  ovn02  47577  rmotru  49912  reutru  49913