Theorem tru 1564

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

Syntax hints:   → wi 4  ∀wal 1558   = wceq 1560  ⊤wtru 1561

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 209  df-tru 1563

This theorem is referenced by:  dftru2  1565  trut  1566  mptru  1567  tbtru  1568  bitru  1569  trud  1570  truan  1571  fal  1574  truorfal  1598  falortru  1599  cadtru  1640  nftru  1824  altru  1827  extru  1995  sbtru  2096  vextru  2747  rextru  3093  rabtru  3648  disjprg  5096  reusv2lem5  5359  rabxfr  5375  reuhyp  5377  euotd  5482  mptexgf  7206  elabrex  7226  elabrexg  7227  caovcl  7590  caovass  7596  caovdi  7615  ectocl  8765  fin1a2lem10  10366  riotaneg  12171  zriotaneg  12686  eflt  16149  efgi0  19760  efgi1  19761  0frgp  19819  mpomulcn  24929  iundisj2  25611  pige3ALT  26585  tanord1  26602  tanord  26603  logtayl  26725  n0sind  28426  nnsind  28466  iundisj2f  32790  iundisj2fi  32999  ordtconn  34222  tgoldbachgt  34957  nexntru  36764  bj-fal  37011  bj-axd2d  37036  bj-rabtr  37415  bj-rabtrALT  37416  bj-dfid2ALT  37550  bj-finsumval0  37777  wl-impchain-mp-x  37941  wl-impchain-com-1.x  37945  wl-impchain-com-n.m  37950  wl-impchain-a1-x  37954  wl-moteq  38017  ftc1anclem5  38196  lhpexle1  40632  3lexlogpow5ineq2  42672  3lexlogpow2ineq1  42675  3lexlogpow2ineq2  42676  mzpcompact2lem  43332  ifpdfor  44041  ifpim1  44045  ifpnot  44046  ifpid2  44047  ifpim2  44048  uun0.1  45353  uunT1  45355  un10  45363  un01  45364  dfbi1ALTa  45515  simprimi  45516  n0abso  45552  liminfvalxr  46357  ovn02  47142  rmotru  49424  reutru  49425