Theorem tru 1479

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

Syntax hints:   → wi 4  ∀wal 1473   = wceq 1475  ⊤wtru 1476

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 196  df-tru 1478

This theorem is referenced by:  fal  1482  dftru2  1483  trud  1484  tbtru  1485  bitru  1487  a1tru  1491  truan  1492  truorfal  1502  falortru  1503  truimfal  1506  cadtru  1550  nftru  1721  disjprg  4578  reusv2lem5  4799  rabxfr  4816  reuhyp  4822  euotd  4900  elabrex  6405  caovcl  6726  caovass  6732  caovdi  6751  ectocl  7702  fin1a2lem10  9114  riotaneg  10879  zriotaneg  11367  cshwsexa  13421  eflt  14686  efgi0  17956  efgi1  17957  0frgp  18015  iundisj2  23124  pige3  24073  tanord1  24087  tanord  24088  logtayl  24206  rabtru  28723  iundisj2f  28785  iundisj2fi  28943  ordtcon  29299  allt  31570  nextnt  31574  bj-trut  31740  bj-axd2d  31750  bj-nftru  31773  bj-extru  31843  bj-rabtr  32118  bj-rabtrALT  32119  bj-rabtrALTALT  32120  bj-df-v  32207  bj-finsumval0  32324  wl-impchain-mp-x  32445  wl-impchain-com-1.x  32449  wl-impchain-com-n.m  32454  wl-impchain-a1-x  32458  ftc1anclem5  32659  lhpexle1  34312  mzpcompact2lem  36332  ifpdfor  36828  ifpim1  36832  ifpnot  36833  ifpid2  36834  ifpim2  36835  uun0.1  38026  uunT1  38028  un10  38036  un01  38037  elabrexg  38229  ovn02  39458