Theorem tru 1537

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

Syntax hints:   → wi 4  ∀wal 1531   = wceq 1533  ⊤wtru 1534

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 1536

This theorem is referenced by:  dftru2  1538  trut  1539  mptru  1540  tbtru  1541  bitru  1542  trud  1543  truan  1544  fal  1547  truorfal  1571  falortru  1572  trunortruOLD  1583  trunorfalOLD  1585  cadtru  1617  nftru  1801  altru  1804  extru  1976  sbtru  2068  vextru  2806  rabtru  3677  disjprgw  5054  disjprg  5055  reusv2lem5  5295  rabxfr  5311  reuhyp  5313  euotd  5396  elabrex  6996  caovcl  7336  caovass  7342  caovdi  7361  ectocl  8359  fin1a2lem10  9825  riotaneg  11614  zriotaneg  12090  cshwsexa  14180  eflt  15464  efgi0  18840  efgi1  18841  0frgp  18899  iundisj2  24144  pige3ALT  25099  tanord1  25115  tanord  25116  logtayl  25237  iundisj2f  30334  iundisj2fi  30514  ordtconn  31163  tgoldbachgt  31929  nexntru  33747  bj-axd2d  33922  bj-rabtr  34243  bj-rabtrALT  34244  bj-df-v  34341  bj-finsumval0  34561  wl-impchain-mp-x  34722  wl-impchain-com-1.x  34726  wl-impchain-com-n.m  34731  wl-impchain-a1-x  34735  wl-moteq  34748  ftc1anclem5  34965  lhpexle1  37138  mzpcompact2lem  39341  ifpdfor  39823  ifpim1  39827  ifpnot  39828  ifpid2  39829  ifpim2  39830  uun0.1  41105  uunT1  41107  un10  41115  un01  41116  elabrexg  41296  liminfvalxr  42056  ovn02  42843