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 230	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 206  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  trunortruOLD  1591  trunorfalOLD  1593  cadtru  1626  nftru  1810  altru  1813  extru  1982  sbtru  2073  vextru  2723  rabtru  3622  ss2abi  4004  ab0orv  4317  disjprgw  5073  disjprg  5074  reusv2lem5  5328  rabxfr  5344  reuhyp  5346  euotd  5429  elabrex  7110  caovcl  7457  caovass  7463  caovdi  7482  ectocl  8548  fin1a2lem10  10149  riotaneg  11937  zriotaneg  12417  cshwsexa  14518  eflt  15807  efgi0  19307  efgi1  19308  0frgp  19366  iundisj2  24694  pige3ALT  25657  tanord1  25674  tanord  25675  logtayl  25796  iundisj2f  30908  iundisj2fi  31097  ordtconn  31854  tgoldbachgt  32622  nexntru  34572  bj-fal  34730  bj-axd2d  34754  bj-rabtr  35097  bj-rabtrALT  35098  bj-dfid2ALT  35215  bj-finsumval0  35435  wl-impchain-mp-x  35597  wl-impchain-com-1.x  35601  wl-impchain-com-n.m  35606  wl-impchain-a1-x  35610  wl-moteq  35652  ftc1anclem5  35833  lhpexle1  38001  3lexlogpow5ineq2  40043  3lexlogpow2ineq1  40046  3lexlogpow2ineq2  40047  mzpcompact2lem  40553  ifpdfor  41034  ifpim1  41038  ifpnot  41039  ifpid2  41040  ifpim2  41041  uun0.1  42351  uunT1  42353  un10  42361  un01  42362  elabrexg  42542  liminfvalxr  43278  ovn02  44060  rextru  46101  rmotru  46102  reutru  46103