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

Theorem 3bitr2i 197
 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 176 . 2 (𝜑𝜒)
4 3bitr2i.3 . 2 (𝜒𝜃)
53, 4bitri 173 1 (𝜑𝜃)
 Colors of variables: wff set class Syntax hints:   ↔ wb 98 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 This theorem is referenced by:  an13  497  sbanv  1769  sbexyz  1879  exists1  1996  euxfrdc  2727  euind  2728  rmo4  2734  rmo3  2849  opm  3971  uniuni  4183  rabxp  4380  eliunxp  4475  dmmrnm  4554  imadisj  4687  intirr  4711  resco  4825  funcnv3  4961  fncnv  4965  fun11  4966  fununi  4967  f1mpt  5410  mpt2mptx  5595  xpcomco  6300  enq0tr  6532  elq  8557
 Copyright terms: Public domain W3C validator