Theorem tru 1368

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

Syntax hints:   → wi 4  ∀wal 1362   = wceq 1364  ⊤wtru 1365

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

This theorem depends on definitions:  df-bi 117  df-tru 1367

This theorem is referenced by:  fal  1371  dftru2  1372  mptru  1373  tbtru  1374  bitru  1376  trud  1380  truan  1381  truorfal  1417  falortru  1418  truimfal  1421  nftru  1480  euotd  4288  rabxfr  4506  reuhyp  4508  elabrex  5807  elabrexg  5808  caovcl  6082  caovass  6088  caovdi  6107  ectocl  6670  reef11  11881  mpomulcn  14886  bj-sbimeh  15502  bdtru  15562  bj-nn0suc0  15680