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  2745  rextru  3093  rabtru  3643  disjprg  5099  reusv2lem5  5367  rabxfr  5383  reuhyp  5385  euotd  5490  mptexgf  7222  elabrex  7240  elabrexg  7241  caovcl  7609  caovass  7615  caovdi  7634  ectocl  8784  fin1a2lem10  10412  riotaneg  12219  zriotaneg  12735  eflt  16206  efgi0  19848  efgi1  19849  0frgp  19907  mpomulcn  25096  iundisj2  25778  pige3ALT  26758  tanord1  26775  tanord  26776  logtayl  26898  n0sind  28599  nnsind  28639  iundisj2f  33064  iundisj2fi  33269  ordtconn  34436  tgoldbachgt  35172  nexntru  37024  bj-fal  37270  bj-axd2d  37295  bj-rabtr  37675  bj-rabtrALT  37676  bj-dfid2ALT  37810  bj-finsumval0  38038  wl-impchain-mp-x  38202  wl-impchain-com-1.x  38206  wl-impchain-com-n.m  38211  wl-impchain-a1-x  38215  wl-moteq  38278  ftc1anclem5  38447  lhpexle1  40882  3lexlogpow5ineq2  42922  3lexlogpow2ineq1  42925  3lexlogpow2ineq2  42926  mzpcompact2lem  43597  ifpdfor  44306  ifpim1  44310  ifpnot  44311  ifpid2  44312  ifpim2  44313  uun0.1  45601  uunT1  45603  un10  45611  un01  45612  dfbi1ALTa  45763  simprimi  45764  n0abso  45800  liminfvalxr  46612  ovn02  47397  rmotru  49732  reutru  49733