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  2722  rextru  3069  rabtru  3633  disjprg  5082  reusv2lem5  5340  rabxfr  5356  reuhyp  5358  euotd  5462  mptexgf  7171  elabrex  7191  elabrexg  7192  caovcl  7555  caovass  7561  caovdi  7580  ectocl  8724  fin1a2lem10  10325  riotaneg  12129  zriotaneg  12636  eflt  16078  efgi0  19689  efgi1  19690  0frgp  19748  mpomulcn  24847  iundisj2  25529  pige3ALT  26500  tanord1  26517  tanord  26518  logtayl  26640  n0sind  28342  nnsind  28382  iundisj2f  32678  iundisj2fi  32888  ordtconn  34088  tgoldbachgt  34826  nexntru  36605  bj-fal  36852  bj-axd2d  36877  bj-rabtr  37256  bj-rabtrALT  37257  bj-dfid2ALT  37391  bj-finsumval0  37618  wl-impchain-mp-x  37780  wl-impchain-com-1.x  37784  wl-impchain-com-n.m  37789  wl-impchain-a1-x  37793  wl-moteq  37856  ftc1anclem5  38035  lhpexle1  40471  3lexlogpow5ineq2  42511  3lexlogpow2ineq1  42514  3lexlogpow2ineq2  42515  mzpcompact2lem  43200  ifpdfor  43913  ifpim1  43917  ifpnot  43918  ifpid2  43919  ifpim2  43920  uun0.1  45225  uunT1  45227  un10  45235  un01  45236  dfbi1ALTa  45387  simprimi  45388  n0abso  45424  liminfvalxr  46232  ovn02  47017  rmotru  49293  reutru  49294