Theorem tru 1526

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

Syntax hints:   → wi 4  ∀wal 1520   = wceq 1522  ⊤wtru 1523

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 1525

This theorem is referenced by:  dftru2  1527  trut  1528  mptru  1529  tbtru  1530  bitru  1531  trud  1532  truan  1533  fal  1536  truorfal  1560  falortru  1561  trunortru  1571  trunorfal  1572  cadtru  1602  nftru  1786  altru  1789  extru  1957  sbtru  2045  vextru  2782  rabtru  3615  disjprg  4958  reusv2lem5  5194  rabxfr  5210  reuhyp  5212  euotd  5294  elabrex  6867  caovcl  7198  caovass  7204  caovdi  7223  ectocl  8215  fin1a2lem10  9677  riotaneg  11468  zriotaneg  11945  cshwsexa  14022  eflt  15303  efgi0  18573  efgi1  18574  0frgp  18632  iundisj2  23833  pige3ALT  24788  tanord1  24802  tanord  24803  logtayl  24924  iundisj2f  30030  iundisj2fi  30206  ordtconn  30785  tgoldbachgt  31551  nexntru  33361  bj-axd2d  33532  bj-rabtr  33819  bj-rabtrALT  33820  bj-df-v  33945  bj-finsumval0  34119  wl-impchain-mp-x  34259  wl-impchain-com-1.x  34263  wl-impchain-com-n.m  34268  wl-impchain-a1-x  34272  wl-moteq  34285  ftc1anclem5  34502  lhpexle1  36675  mzpcompact2lem  38833  ifpdfor  39315  ifpim1  39319  ifpnot  39320  ifpid2  39321  ifpim2  39322  uun0.1  40651  uunT1  40653  un10  40661  un01  40662  elabrexg  40842  liminfvalxr  41606  ovn02  42392