Theorem tru 1335

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

Syntax hints:   → wi 4  ∀wal 1329   = wceq 1331  ⊤wtru 1332

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 1334

This theorem is referenced by:  fal  1338  dftru2  1339  mptru  1340  tbtru  1341  bitru  1343  a1tru  1347  truan  1348  truorfal  1384  falortru  1385  truimfal  1388  nftru  1442  euotd  4171  rabxfr  4386  reuhyp  4388  elabrex  5652  caovcl  5918  caovass  5924  caovdi  5943  ectocl  6489  reef11  11395  bj-sbimeh  12968  bdtru  13019  bj-nn0suc0  13137