Theorem tru 1545

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

Syntax hints:   → wi 4  ∀wal 1539   = wceq 1541  ⊤wtru 1542

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 1544

This theorem is referenced by:  dftru2  1546  trut  1547  mptru  1548  tbtru  1549  bitru  1550  trud  1551  truan  1552  fal  1555  truorfal  1579  falortru  1580  cadtru  1621  nftru  1805  altru  1808  extru  1976  sbtru  2072  vextru  2721  rextru  3067  rabtru  3644  ss2abi  4018  disjprg  5094  reusv2lem5  5347  rabxfr  5363  reuhyp  5365  euotd  5461  mptexgf  7168  elabrex  7188  elabrexg  7189  caovcl  7552  caovass  7558  caovdi  7577  ectocl  8720  fin1a2lem10  10319  riotaneg  12121  zriotaneg  12605  eflt  16042  efgi0  19649  efgi1  19650  0frgp  19708  mpomulcn  24814  iundisj2  25506  pige3ALT  26485  tanord1  26502  tanord  26503  logtayl  26625  n0sind  28329  nnsind  28369  iundisj2f  32665  iundisj2fi  32877  ordtconn  34082  tgoldbachgt  34820  nexntru  36598  bj-fal  36770  bj-axd2d  36793  bj-rabtr  37131  bj-rabtrALT  37132  bj-dfid2ALT  37266  bj-finsumval0  37490  wl-impchain-mp-x  37652  wl-impchain-com-1.x  37656  wl-impchain-com-n.m  37661  wl-impchain-a1-x  37665  wl-moteq  37719  ftc1anclem5  37898  lhpexle1  40278  3lexlogpow5ineq2  42319  3lexlogpow2ineq1  42322  3lexlogpow2ineq2  42323  mzpcompact2lem  43003  ifpdfor  43716  ifpim1  43720  ifpnot  43721  ifpid2  43722  ifpim2  43723  uun0.1  45028  uunT1  45030  un10  45038  un01  45039  dfbi1ALTa  45190  simprimi  45191  n0abso  45227  liminfvalxr  46037  ovn02  46822  rmotru  49058  reutru  49059