Theorem tru 1347

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

Syntax hints:   → wi 4  ∀wal 1341   = wceq 1343  ⊤wtru 1344

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

This theorem depends on definitions:  df-bi 116  df-tru 1346

This theorem is referenced by:  fal  1350  dftru2  1351  mptru  1352  tbtru  1353  bitru  1355  a1tru  1359  truan  1360  truorfal  1396  falortru  1397  truimfal  1400  nftru  1454  euotd  4232  rabxfr  4448  reuhyp  4450  elabrex  5726  caovcl  5996  caovass  6002  caovdi  6021  ectocl  6568  reef11  11640  bj-sbimeh  13653  bdtru  13714  bj-nn0suc0  13832