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  528  sbanv  1812  sbexyz  1922  exists1  2039  euxfrdc  2789  euind  2790  rmo4  2796  rmo3  2916  ddifstab  3116  opm  4025  uniuni  4237  rabxp  4436  eliunxp  4533  dmmrnm  4613  imadisj  4749  intirr  4773  resco  4889  funcnv3  5029  fncnv  5033  fun11  5034  fununi  5035  f1mpt  5490  mpt2mptx  5674  mapsnen  6458  xpcomco  6472  enq0tr  6896  elq  9002
  Copyright terms: Public domain W3C validator