Theorem tru 1544

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 22	. 2 ⊢ (∀𝑥 𝑥 = 𝑥 → ∀𝑥 𝑥 = 𝑥)
2		df-tru 1543	. 2 ⊢ (⊤ ↔ (∀𝑥 𝑥 = 𝑥 → ∀𝑥 𝑥 = 𝑥))
3	1, 2	mpbir 231	1 ⊢ ⊤

Syntax hints:   → wi 4  ∀wal 1538   = wceq 1540  ⊤wtru 1541

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 207  df-tru 1543

This theorem is referenced by:  dftru2  1545  trut  1546  mptru  1547  tbtru  1548  bitru  1549  trud  1550  truan  1551  fal  1554  truorfal  1578  falortru  1579  cadtru  1620  nftru  1804  altru  1807  extru  1975  sbtru  2067  vextru  2720  rextru  3067  rabtru  3668  ss2abi  4042  ab0orv  4358  disjprg  5115  reusv2lem5  5372  rabxfr  5388  reuhyp  5390  euotd  5488  mptexgf  7214  elabrex  7234  elabrexg  7235  caovcl  7601  caovass  7607  caovdi  7626  ectocl  8799  fin1a2lem10  10423  riotaneg  12221  zriotaneg  12706  cshwsexaOLD  14843  eflt  16135  efgi0  19701  efgi1  19702  0frgp  19760  mpomulcn  24809  iundisj2  25502  pige3ALT  26481  tanord1  26498  tanord  26499  logtayl  26621  n0sind  28277  nnsind  28314  iundisj2f  32571  iundisj2fi  32774  ordtconn  33956  tgoldbachgt  34695  nexntru  36422  bj-fal  36588  bj-axd2d  36611  bj-rabtr  36948  bj-rabtrALT  36949  bj-dfid2ALT  37083  bj-finsumval0  37303  wl-impchain-mp-x  37465  wl-impchain-com-1.x  37469  wl-impchain-com-n.m  37474  wl-impchain-a1-x  37478  wl-moteq  37532  ftc1anclem5  37721  lhpexle1  40027  3lexlogpow5ineq2  42068  3lexlogpow2ineq1  42071  3lexlogpow2ineq2  42072  mzpcompact2lem  42774  ifpdfor  43489  ifpim1  43493  ifpnot  43494  ifpid2  43495  ifpim2  43496  uun0.1  44802  uunT1  44804  un10  44812  un01  44813  dfbi1ALTa  44964  simprimi  44965  n0abso  45001  liminfvalxr  45812  ovn02  46597  rmotru  48782  reutru  48783