Theorem tru 1571

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

Syntax hints:   → wi 4  ∀wal 1565   = wceq 1567  ⊤wtru 1568

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 1570

This theorem is referenced by:  dftru2  1572  trut  1573  mptru  1574  tbtru  1575  bitru  1576  trud  1577  truan  1578  fal  1581  truorfal  1605  falortru  1606  cadtru  1647  nftru  1831  altru  1834  extru  2002  sbtru  2103  vextru  2754  rextru  3102  rabtru  3657  disjprg  5109  reusv2lem5  5374  rabxfr  5390  reuhyp  5392  euotd  5497  mptexgf  7221  elabrex  7241  elabrexg  7242  caovcl  7605  caovass  7611  caovdi  7630  ectocl  8781  fin1a2lem10  10393  riotaneg  12194  zriotaneg  12709  eflt  16173  efgi0  19790  efgi1  19791  0frgp  19849  mpomulcn  24995  iundisj2  25677  pige3ALT  26651  tanord1  26668  tanord  26669  logtayl  26791  n0sind  28492  nnsind  28532  iundisj2f  32876  iundisj2fi  33083  ordtconn  34260  tgoldbachgt  34995  nexntru  36804  bj-fal  37050  bj-axd2d  37075  bj-rabtr  37454  bj-rabtrALT  37455  bj-dfid2ALT  37589  bj-finsumval0  37817  wl-impchain-mp-x  37981  wl-impchain-com-1.x  37985  wl-impchain-com-n.m  37990  wl-impchain-a1-x  37994  wl-moteq  38057  ftc1anclem5  38236  lhpexle1  40672  3lexlogpow5ineq2  42712  3lexlogpow2ineq1  42715  3lexlogpow2ineq2  42716  mzpcompact2lem  43374  ifpdfor  44083  ifpim1  44087  ifpnot  44088  ifpid2  44089  ifpim2  44090  uun0.1  45378  uunT1  45380  un10  45388  un01  45389  dfbi1ALTa  45540  simprimi  45541  n0abso  45577  liminfvalxr  46389  ovn02  47174  rmotru  49466  reutru  49467