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

Theorem 3bitr2i 207
Description: A chained inference from transitive law for logical equivalence. (Contributed by NM, 4-Aug-2006.)
Hypotheses
Ref Expression
3bitr2i.1 (𝜑𝜓)
3bitr2i.2 (𝜒𝜓)
3bitr2i.3 (𝜒𝜃)
Assertion
Ref Expression
3bitr2i (𝜑𝜃)

Proof of Theorem 3bitr2i
StepHypRef Expression
1 3bitr2i.1 . . 3 (𝜑𝜓)
2 3bitr2i.2 . . 3 (𝜒𝜓)
31, 2bitr4i 186 . 2 (𝜑𝜒)
4 3bitr2i.3 . 2 (𝜒𝜃)
53, 4bitri 183 1 (𝜑𝜃)
Colors of variables: wff set class
Syntax hints:  wb 104
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
This theorem is referenced by:  an13  558  sbanv  1882  sbexyz  1996  exists1  2115  euxfrdc  2916  euind  2917  rmo4  2923  rmo3f  2927  rmo3  3046  ddifstab  3259  opm  4217  uniuni  4434  rabxp  4646  eliunxp  4748  dmmrnm  4828  imadisj  4971  intirr  4995  resco  5113  funcnv3  5258  fncnv  5262  fun11  5263  fununi  5264  f1mpt  5748  mpomptx  5942  ixp0x  6702  mapsnen  6787  xpcomco  6802  enq0tr  7389  elq  9574  pythagtrip  12230  ntreq0  12891  tx1cn  13028
  Copyright terms: Public domain W3C validator