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

Theorem 3bitr2i 206
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 185 . 2 (𝜑𝜒)
4 3bitr2i.3 . 2 (𝜒𝜃)
53, 4bitri 182 1 (𝜑𝜃)
Colors of variables: wff set class
Syntax hints:  wb 103
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106
This theorem depends on definitions:  df-bi 115
This theorem is referenced by:  an13  530  sbanv  1817  sbexyz  1927  exists1  2044  euxfrdc  2801  euind  2802  rmo4  2808  rmo3f  2812  rmo3  2930  ddifstab  3132  opm  4061  uniuni  4273  rabxp  4474  eliunxp  4575  dmmrnm  4655  imadisj  4794  intirr  4818  resco  4935  funcnv3  5076  fncnv  5080  fun11  5081  fununi  5082  f1mpt  5550  mpt2mptx  5739  mapsnen  6528  xpcomco  6542  enq0tr  6993  elq  9107
  Copyright terms: Public domain W3C validator