Theorem tru 1247

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

Syntax hints:   → wi 4  ∀wal 1241   = wceq 1243  ⊤wtru 1244

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101

This theorem depends on definitions:  df-bi 110  df-tru 1246

This theorem is referenced by:  fal  1250  dftru2  1251  trud  1252  tbtru  1253  bitru  1255  a1tru  1259  truan  1260  truorfal  1297  falortru  1298  truimfal  1301  nftru  1355  euotd  3991  rabxfr  4202  reuhyp  4204  elabrex  5397  caovcl  5655  caovass  5661  caovdi  5680  ectocl  6173  bj-sbimeh  9912  bdtru  9952  bj-nn0suc0  10075