Theorem tru 1543

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

Syntax hints:   → wi 4  ∀wal 1537   = wceq 1539  ⊤wtru 1540

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 1542

This theorem is referenced by:  dftru2  1544  trut  1545  mptru  1546  tbtru  1547  bitru  1548  trud  1549  truan  1550  fal  1553  truorfal  1577  falortru  1578  cadtru  1620  nftru  1804  altru  1807  extru  1977  sbtru  2068  vextru  2720  rabtru  3626  ss2abi  4005  ab0orv  4318  disjprgw  5076  disjprg  5077  reusv2lem5  5334  rabxfr  5350  reuhyp  5352  euotd  5440  mptexgf  7130  elabrex  7148  caovcl  7498  caovass  7504  caovdi  7523  ectocl  8605  fin1a2lem10  10211  riotaneg  12000  zriotaneg  12481  cshwsexa  14582  eflt  15871  efgi0  19371  efgi1  19372  0frgp  19430  iundisj2  24758  pige3ALT  25721  tanord1  25738  tanord  25739  logtayl  25860  iundisj2f  30974  iundisj2fi  31163  ordtconn  31920  tgoldbachgt  32688  nexntru  34638  bj-fal  34796  bj-axd2d  34820  bj-rabtr  35162  bj-rabtrALT  35163  bj-dfid2ALT  35280  bj-finsumval0  35500  wl-impchain-mp-x  35662  wl-impchain-com-1.x  35666  wl-impchain-com-n.m  35671  wl-impchain-a1-x  35675  wl-moteq  35717  ftc1anclem5  35898  lhpexle1  38064  3lexlogpow5ineq2  40105  3lexlogpow2ineq1  40108  3lexlogpow2ineq2  40109  mzpcompact2lem  40610  ifpdfor  41110  ifpim1  41114  ifpnot  41115  ifpid2  41116  ifpim2  41117  uun0.1  42436  uunT1  42438  un10  42446  un01  42447  elabrexg  42627  liminfvalxr  43373  ovn02  44156  rextru  46207  rmotru  46208  reutru  46209