Theorem tru 1288

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

Syntax hints:   → wi 4  ∀wal 1282   = wceq 1284  ⊤wtru 1285

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 1287

This theorem is referenced by:  fal  1291  dftru2  1292  trud  1293  tbtru  1294  bitru  1296  a1tru  1300  truan  1301  truorfal  1337  falortru  1338  truimfal  1341  nftru  1395  euotd  4009  rabxfr  4220  reuhyp  4222  elabrex  5418  caovcl  5675  caovass  5681  caovdi  5700  ectocl  6196  bj-sbimeh  10583  bdtru  10623  bj-nn0suc0  10745