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 231	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 207  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  1622  nftru  1806  altru  1809  extru  1977  sbtru  2073  vextru  2721  rextru  3068  rabtru  3632  disjprg  5081  reusv2lem5  5344  rabxfr  5360  reuhyp  5362  euotd  5467  mptexgf  7177  elabrex  7197  elabrexg  7198  caovcl  7561  caovass  7567  caovdi  7586  ectocl  8730  fin1a2lem10  10331  riotaneg  12135  zriotaneg  12642  eflt  16084  efgi0  19695  efgi1  19696  0frgp  19754  mpomulcn  24834  iundisj2  25516  pige3ALT  26484  tanord1  26501  tanord  26502  logtayl  26624  n0sind  28325  nnsind  28365  iundisj2f  32660  iundisj2fi  32870  ordtconn  34069  tgoldbachgt  34807  nexntru  36586  bj-fal  36833  bj-axd2d  36858  bj-rabtr  37237  bj-rabtrALT  37238  bj-dfid2ALT  37372  bj-finsumval0  37599  wl-impchain-mp-x  37763  wl-impchain-com-1.x  37767  wl-impchain-com-n.m  37772  wl-impchain-a1-x  37776  wl-moteq  37839  ftc1anclem5  38018  lhpexle1  40454  3lexlogpow5ineq2  42494  3lexlogpow2ineq1  42497  3lexlogpow2ineq2  42498  mzpcompact2lem  43183  ifpdfor  43892  ifpim1  43896  ifpnot  43897  ifpid2  43898  ifpim2  43899  uun0.1  45204  uunT1  45206  un10  45214  un01  45215  dfbi1ALTa  45366  simprimi  45367  n0abso  45403  liminfvalxr  46211  ovn02  46996  rmotru  49278  reutru  49279