Theorem tru 1487

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

Syntax hints:   → wi 4  ∀wal 1481   = wceq 1483  ⊤wtru 1484

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 197  df-tru 1486

This theorem is referenced by:  fal  1490  dftru2  1491  trut  1492  trud  1493  tbtru  1494  bitru  1496  a1tru  1500  truan  1501  truorfal  1511  falortru  1512  cadtru  1559  nftru  1730  rabtru  3361  disjprg  4648  reusv2lem5  4873  rabxfr  4890  reuhyp  4896  euotd  4975  elabrex  6501  caovcl  6828  caovass  6834  caovdi  6853  ectocl  7815  fin1a2lem10  9231  riotaneg  11002  zriotaneg  11491  cshwsexa  13570  eflt  14847  efgi0  18133  efgi1  18134  0frgp  18192  iundisj2  23317  pige3  24269  tanord1  24283  tanord  24284  logtayl  24406  iundisj2f  29403  iundisj2fi  29556  ordtconn  29971  tgoldbachgt  30741  allt  32400  nextnt  32404  bj-axd2d  32577  bj-extru  32654  bj-rabtr  32926  bj-rabtrALT  32927  bj-rabtrALTALT  32928  bj-df-v  33016  bj-finsumval0  33147  wl-impchain-mp-x  33269  wl-impchain-com-1.x  33273  wl-impchain-com-n.m  33278  wl-impchain-a1-x  33282  ftc1anclem5  33489  lhpexle1  35294  mzpcompact2lem  37314  ifpdfor  37809  ifpim1  37813  ifpnot  37814  ifpid2  37815  ifpim2  37816  uun0.1  39005  uunT1  39007  un10  39015  un01  39016  elabrexg  39206  liminfvalxr  40015  ovn02  40782