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

Theorem tru 1368
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 1367 . 2 (⊤ ↔ (∀𝑥 𝑥 = 𝑥 → ∀𝑥 𝑥 = 𝑥))
31, 2mpbir 146 1
Colors of variables: wff set class
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  1477  euotd  4272  rabxfr  4488  reuhyp  4490  elabrex  5779  elabrexg  5780  caovcl  6052  caovass  6058  caovdi  6077  ectocl  6629  reef11  11742  bj-sbimeh  15002  bdtru  15062  bj-nn0suc0  15180
  Copyright terms: Public domain W3C validator