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

Theorem tru 1303
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 1302 . 2 (⊤ ↔ (∀𝑥 𝑥 = 𝑥 → ∀𝑥 𝑥 = 𝑥))
31, 2mpbir 145 1
Colors of variables: wff set class
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
  Copyright terms: Public domain W3C validator