Theorem tru 1303

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

Syntax hints:   → wi 4  ∀wal 1297   = wceq 1299  ⊤wtru 1300

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

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

This theorem is referenced by:  fal  1306  dftru2  1307  mptru  1308  tbtru  1309  bitru  1311  a1tru  1315  truan  1316  truorfal  1352  falortru  1353  truimfal  1356  nftru  1410  euotd  4114  rabxfr  4329  reuhyp  4331  elabrex  5591  caovcl  5857  caovass  5863  caovdi  5882  ectocl  6426  reef11  11204  bj-sbimeh  12561  bdtru  12611  bj-nn0suc0  12733