Theorem tru 1551

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

Syntax hints:   → wi 4  ∀wal 1545   = wceq 1547  ⊤wtru 1548

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 208  df-tru 1550

This theorem is referenced by:  dftru2  1552  trut  1553  mptru  1554  tbtru  1555  bitru  1556  trud  1557  truan  1558  fal  1561  truorfal  1585  falortru  1586  cadtru  1627  nftru  1811  altru  1814  extru  1982  sbtru  2078  vextru  2724  rextru  3070  rabtru  3627  disjprg  5068  reusv2lem5  5331  rabxfr  5347  reuhyp  5349  euotd  5454  mptexgf  7166  elabrex  7186  elabrexg  7187  caovcl  7550  caovass  7556  caovdi  7575  ectocl  8720  fin1a2lem10  10322  riotaneg  12126  zriotaneg  12633  eflt  16075  efgi0  19686  efgi1  19687  0frgp  19745  mpomulcn  24852  iundisj2  25534  pige3ALT  26502  tanord1  26519  tanord  26520  logtayl  26642  n0sind  28343  nnsind  28383  iundisj2f  32679  iundisj2fi  32889  ordtconn  34109  tgoldbachgt  34847  nexntru  36632  bj-fal  36879  bj-axd2d  36904  bj-rabtr  37283  bj-rabtrALT  37284  bj-dfid2ALT  37418  bj-finsumval0  37645  wl-impchain-mp-x  37809  wl-impchain-com-1.x  37813  wl-impchain-com-n.m  37818  wl-impchain-a1-x  37822  wl-moteq  37885  ftc1anclem5  38064  lhpexle1  40500  3lexlogpow5ineq2  42540  3lexlogpow2ineq1  42543  3lexlogpow2ineq2  42544  mzpcompact2lem  43200  ifpdfor  43909  ifpim1  43913  ifpnot  43914  ifpid2  43915  ifpim2  43916  uun0.1  45221  uunT1  45223  un10  45231  un01  45232  dfbi1ALTa  45383  simprimi  45384  n0abso  45420  liminfvalxr  46226  ovn02  47011  rmotru  49293  reutru  49294