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

Theorem 3bitr2i 201
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 180 . 2 (𝜑𝜒)
4 3bitr2i.3 . 2 (𝜒𝜃)
53, 4bitri 177 1 (𝜑𝜃)
Colors of variables: wff set class
Syntax hints:  wb 102
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 103  ax-ia2 104  ax-ia3 105
This theorem depends on definitions:  df-bi 114
This theorem is referenced by:  an13  505  sbanv  1785  sbexyz  1895  exists1  2012  euxfrdc  2749  euind  2750  rmo4  2756  rmo3  2876  opm  3998  uniuni  4210  rabxp  4407  eliunxp  4502  dmmrnm  4581  imadisj  4714  intirr  4738  resco  4852  funcnv3  4988  fncnv  4992  fun11  4993  fununi  4994  f1mpt  5437  mpt2mptx  5622  xpcomco  6330  enq0tr  6589  elq  8653
  Copyright terms: Public domain W3C validator