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  4219  uniuni  4436  rabxp  4648  eliunxp  4750  dmmrnm  4830  imadisj  4973  intirr  4997  resco  5115  funcnv3  5260  fncnv  5264  fun11  5265  fununi  5266  f1mpt  5750  mpomptx  5944  ixp0x  6704  mapsnen  6789  xpcomco  6804  enq0tr  7396  elq  9581  pythagtrip  12237  ntreq0  12926  tx1cn  13063
  Copyright terms: Public domain W3C validator