Theorem tru 1289

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 19	. 2 ⊢ (∀𝑥 𝑥 = 𝑥 → ∀𝑥 𝑥 = 𝑥)
2		df-tru 1288	. 2 ⊢ (⊤ ↔ (∀𝑥 𝑥 = 𝑥 → ∀𝑥 𝑥 = 𝑥))
3	1, 2	mpbir 144	1 ⊢ ⊤

Syntax hints:   → wi 4  ∀wal 1283   = wceq 1285  ⊤wtru 1286

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106

This theorem depends on definitions:  df-bi 115  df-tru 1288

This theorem is referenced by:  fal  1292  dftru2  1293  trud  1294  tbtru  1295  bitru  1297  a1tru  1301  truan  1302  truorfal  1338  falortru  1339  truimfal  1342  nftru  1396  euotd  4044  rabxfr  4255  reuhyp  4257  elabrex  5475  caovcl  5732  caovass  5738  caovdi  5757  ectocl  6287  bj-sbimeh  11014  bdtru  11064  bj-nn0suc0  11186