Theorem tru 1377

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

Syntax hints:   → wi 4  ∀wal 1371   = wceq 1373  ⊤wtru 1374

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 1376

This theorem is referenced by:  fal  1380  dftru2  1381  mptru  1382  tbtru  1383  bitru  1385  trud  1389  truan  1390  truorfal  1426  falortru  1427  truimfal  1430  nftru  1489  euotd  4299  rabxfr  4517  reuhyp  4519  elabrex  5826  elabrexg  5827  caovcl  6101  caovass  6107  caovdi  6126  ectocl  6689  reef11  12010  mpomulcn  15038  bj-sbimeh  15708  bdtru  15768  bj-nn0suc0  15886