Theorem tru 1573

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

This proof depends on syntax axioms:   → wi 4  ∀wal 1567   = wceq 1569  ⊤wtru 1570

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 1572

This theorem is used by:  dftru2  1574  trut  1575  mptru  1576  tbtru  1577  bitru  1578  trud  1579  truan  1580  fal  1583  truorfal  1607  falortru  1608  cadtru  1652  nftru  1836  altru  1839  extru  2007  sbtru  2103  vextru  2745  rextru  3093  rabtru  3642  disjprg  5098  reusv2lem5  5364  rabxfr  5380  reuhyp  5382  euotd  5486  mptexgf  7232  elabrex  7250  elabrexg  7251  caovcl  7619  caovass  7625  caovdi  7644  ectocl  8812  fin1a2lem10  10494  riotaneg  12303  zriotaneg  12819  eflt  16294  efgi0  19943  efgi1  19944  0frgp  20002  mpomulcn  25197  iundisj2  25879  pige3ALT  26857  tanord1  26874  tanord  26875  logtayl  26997  n0sind  28728  nnsind  28768  iundisj2f  33235  iundisj2fi  33439  ordtconn  34607  tgoldbachgt  35342  nexntru  37316  bj-fal  37562  bj-axd2d  37587  bj-rabtr  37967  bj-rabtrALT  37968  bj-dfid2ALT  38116  bj-finsumval0  38343  wl-impchain-mp-x  38507  wl-impchain-com-1.x  38511  wl-impchain-com-n.m  38516  wl-impchain-a1-x  38520  wl-moteq  38583  ftc1anclem5  38752  lhpexle1  41202  3lexlogpow5ineq2  43242  3lexlogpow2ineq1  43245  3lexlogpow2ineq2  43246  mzpcompact2lem  43899  ifpdfor  44603  ifpim1  44607  ifpnot  44608  ifpid2  44609  ifpim2  44610  uun0.1  45896  uunT1  45898  un10  45906  un01  45907  dfbi1ALTa  46065  simprimi  46066  n0abso  46102  liminfvalxr  46929  ovn02  47714  rmotru  50049  reutru  50050