Theorem tru 1546

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

Syntax hints:   → wi 4  ∀wal 1540   = wceq 1542  ⊤wtru 1543

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 206  df-tru 1545

This theorem is referenced by:  dftru2  1547  trut  1548  mptru  1549  tbtru  1550  bitru  1551  trud  1552  truan  1553  fal  1556  truorfal  1580  falortru  1581  cadtru  1623  nftru  1807  altru  1810  extru  1980  sbtru  2071  vextru  2717  rextru  3078  rabtru  3681  ss2abi  4064  ab0orv  4379  disjprgw  5144  disjprg  5145  reusv2lem5  5401  rabxfr  5417  reuhyp  5419  euotd  5514  mptexgf  7224  elabrex  7242  caovcl  7601  caovass  7607  caovdi  7626  ectocl  8779  fin1a2lem10  10404  riotaneg  12193  zriotaneg  12675  cshwsexaOLD  14775  eflt  16060  efgi0  19588  efgi1  19589  0frgp  19647  iundisj2  25066  pige3ALT  26029  tanord1  26046  tanord  26047  logtayl  26168  iundisj2f  31821  iundisj2fi  32008  ordtconn  32905  tgoldbachgt  33675  nexntru  35289  bj-fal  35447  bj-axd2d  35471  bj-rabtr  35810  bj-rabtrALT  35811  bj-dfid2ALT  35946  bj-finsumval0  36166  wl-impchain-mp-x  36328  wl-impchain-com-1.x  36332  wl-impchain-com-n.m  36337  wl-impchain-a1-x  36341  wl-moteq  36383  ftc1anclem5  36565  lhpexle1  38879  3lexlogpow5ineq2  40920  3lexlogpow2ineq1  40923  3lexlogpow2ineq2  40924  mzpcompact2lem  41489  ifpdfor  42216  ifpim1  42220  ifpnot  42221  ifpid2  42222  ifpim2  42223  uun0.1  43539  uunT1  43541  un10  43549  un01  43550  elabrexg  43728  liminfvalxr  44499  ovn02  45284  rmotru  47489  reutru  47490