Theorem tru 1567

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

Syntax hints:   → wi 4  ∀wal 1561   = wceq 1563  ⊤wtru 1564

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 1566

This theorem is referenced by:  dftru2  1568  trut  1569  mptru  1570  tbtru  1571  bitru  1572  trud  1573  truan  1574  fal  1577  truorfal  1601  falortru  1602  cadtru  1643  nftru  1827  altru  1830  extru  1998  sbtru  2099  vextru  2750  rextru  3096  rabtru  3651  disjprg  5100  reusv2lem5  5363  rabxfr  5379  reuhyp  5381  euotd  5486  mptexgf  7210  elabrex  7230  elabrexg  7231  caovcl  7594  caovass  7600  caovdi  7619  ectocl  8769  fin1a2lem10  10381  riotaneg  12182  zriotaneg  12697  eflt  16161  efgi0  19778  efgi1  19779  0frgp  19837  mpomulcn  24983  iundisj2  25665  pige3ALT  26639  tanord1  26656  tanord  26657  logtayl  26779  n0sind  28480  nnsind  28520  iundisj2f  32841  iundisj2fi  33050  ordtconn  34227  tgoldbachgt  34962  nexntru  36772  bj-fal  37018  bj-axd2d  37043  bj-rabtr  37422  bj-rabtrALT  37423  bj-dfid2ALT  37557  bj-finsumval0  37784  wl-impchain-mp-x  37948  wl-impchain-com-1.x  37952  wl-impchain-com-n.m  37957  wl-impchain-a1-x  37961  wl-moteq  38024  ftc1anclem5  38203  lhpexle1  40639  3lexlogpow5ineq2  42679  3lexlogpow2ineq1  42682  3lexlogpow2ineq2  42683  mzpcompact2lem  43339  ifpdfor  44048  ifpim1  44052  ifpnot  44053  ifpid2  44054  ifpim2  44055  uun0.1  45345  uunT1  45347  un10  45355  un01  45356  dfbi1ALTa  45507  simprimi  45508  n0abso  45544  liminfvalxr  46356  ovn02  47141  rmotru  49433  reutru  49434