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

Theorem tru 1320
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 1319 . 2 (⊤ ↔ (∀𝑥 𝑥 = 𝑥 → ∀𝑥 𝑥 = 𝑥))
31, 2mpbir 145 1
Colors of variables: wff set class
Syntax hints:  wi 4  wal 1314   = wceq 1316  wtru 1317
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 1319
This theorem is referenced by:  fal  1323  dftru2  1324  mptru  1325  tbtru  1326  bitru  1328  a1tru  1332  truan  1333  truorfal  1369  falortru  1370  truimfal  1373  nftru  1427  euotd  4146  rabxfr  4361  reuhyp  4363  elabrex  5627  caovcl  5893  caovass  5899  caovdi  5918  ectocl  6464  reef11  11320  bj-sbimeh  12875  bdtru  12926  bj-nn0suc0  13044
  Copyright terms: Public domain W3C validator