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

Theorem tru 1246
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 1245 . 2
31, 2mpbir 134 1
Colors of variables: wff set class
Syntax hints:   wi 4  wal 1240   wceq 1242   wtru 1243
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101
This theorem depends on definitions:  df-bi 110  df-tru 1245
This theorem is referenced by:  fal  1249  dftru2  1250  trud  1251  tbtru  1252  bitru  1254  a1tru  1258  truan  1259  truorfal  1294  falortru  1295  truimfal  1298  nftru  1352  euotd  3982  rabxfr  4168  reuhyp  4170  elabrex  5340  caovcl  5597  caovass  5603  caovdi  5622  ectocl  6109  bj-sbimeh  9181  bdtru  9221  bj-nn0suc0  9338
  Copyright terms: Public domain W3C validator