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  2750  rextru  3098  rabtru  3650  disjprg  5107  reusv2lem5  5375  rabxfr  5391  reuhyp  5393  euotd  5498  mptexgf  7227  elabrex  7245  elabrexg  7246  caovcl  7614  caovass  7620  caovdi  7639  ectocl  8787  fin1a2lem10  10408  riotaneg  12211  zriotaneg  12727  eflt  16197  efgi0  19836  efgi1  19837  0frgp  19895  mpomulcn  25079  iundisj2  25761  pige3ALT  26738  tanord1  26755  tanord  26756  logtayl  26878  n0sind  28579  nnsind  28619  iundisj2f  33008  iundisj2fi  33214  ordtconn  34381  tgoldbachgt  35117  nexntru  36974  bj-fal  37220  bj-axd2d  37245  bj-rabtr  37625  bj-rabtrALT  37626  bj-dfid2ALT  37760  bj-finsumval0  37988  wl-impchain-mp-x  38152  wl-impchain-com-1.x  38156  wl-impchain-com-n.m  38161  wl-impchain-a1-x  38165  wl-moteq  38228  ftc1anclem5  38407  lhpexle1  40842  3lexlogpow5ineq2  42882  3lexlogpow2ineq1  42885  3lexlogpow2ineq2  42886  mzpcompact2lem  43542  ifpdfor  44251  ifpim1  44255  ifpnot  44256  ifpid2  44257  ifpim2  44258  uun0.1  45546  uunT1  45548  un10  45556  un01  45557  dfbi1ALTa  45708  simprimi  45709  n0abso  45745  liminfvalxr  46557  ovn02  47342  rmotru  49640  reutru  49641