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  2068  vextru  2714  rextru  3060  rabtru  3653  ss2abi  4027  ab0orv  4342  disjprg  5098  reusv2lem5  5352  rabxfr  5368  reuhyp  5370  euotd  5468  mptexgf  7178  elabrex  7198  elabrexg  7199  caovcl  7563  caovass  7569  caovdi  7588  ectocl  8733  fin1a2lem10  10338  riotaneg  12138  zriotaneg  12623  cshwsexaOLD  14766  eflt  16061  efgi0  19634  efgi1  19635  0frgp  19693  mpomulcn  24791  iundisj2  25483  pige3ALT  26462  tanord1  26479  tanord  26480  logtayl  26602  n0sind  28265  nnsind  28302  iundisj2f  32569  iundisj2fi  32770  ordtconn  33908  tgoldbachgt  34647  nexntru  36385  bj-fal  36551  bj-axd2d  36574  bj-rabtr  36911  bj-rabtrALT  36912  bj-dfid2ALT  37046  bj-finsumval0  37266  wl-impchain-mp-x  37428  wl-impchain-com-1.x  37432  wl-impchain-com-n.m  37437  wl-impchain-a1-x  37441  wl-moteq  37495  ftc1anclem5  37684  lhpexle1  39995  3lexlogpow5ineq2  42036  3lexlogpow2ineq1  42039  3lexlogpow2ineq2  42040  mzpcompact2lem  42732  ifpdfor  43447  ifpim1  43451  ifpnot  43452  ifpid2  43453  ifpim2  43454  uun0.1  44760  uunT1  44762  un10  44770  un01  44771  dfbi1ALTa  44922  simprimi  44923  n0abso  44959  liminfvalxr  45774  ovn02  46559  rmotru  48784  reutru  48785