ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  tru GIF version

Theorem tru 1289
Description: The truth value is provable. (Contributed by Anthony Hart, 13-Oct-2010.)
Assertion
Ref Expression
tru

Proof of Theorem tru
StepHypRef Expression
1 id 19 . 2 (∀𝑥 𝑥 = 𝑥 → ∀𝑥 𝑥 = 𝑥)
2 df-tru 1288 . 2 (⊤ ↔ (∀𝑥 𝑥 = 𝑥 → ∀𝑥 𝑥 = 𝑥))
31, 2mpbir 144 1
Colors of variables: wff set class
Syntax hints:  wi 4  wal 1283   = wceq 1285  wtru 1286
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 1288
This theorem is referenced by:  fal  1292  dftru2  1293  trud  1294  tbtru  1295  bitru  1297  a1tru  1301  truan  1302  truorfal  1338  falortru  1339  truimfal  1342  nftru  1396  euotd  4044  rabxfr  4255  reuhyp  4257  elabrex  5475  caovcl  5732  caovass  5738  caovdi  5757  ectocl  6287  bj-sbimeh  11014  bdtru  11064  bj-nn0suc0  11186
  Copyright terms: Public domain W3C validator