Theorem tru 1352

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

Syntax hints:   → wi 4  ∀wal 1346   = wceq 1348  ⊤wtru 1349

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 1351

This theorem is referenced by:  fal  1355  dftru2  1356  mptru  1357  tbtru  1358  bitru  1360  a1tru  1364  truan  1365  truorfal  1401  falortru  1402  truimfal  1405  nftru  1459  euotd  4239  rabxfr  4455  reuhyp  4457  elabrex  5737  caovcl  6007  caovass  6013  caovdi  6032  ectocl  6580  reef11  11662  bj-sbimeh  13807  bdtru  13867  bj-nn0suc0  13985