ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  3bitr2i Unicode 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  |-  ( ph  <->  ps )
3bitr2i.2  |-  ( ch  <->  ps )
3bitr2i.3  |-  ( ch  <->  th )
Assertion
Ref Expression
3bitr2i  |-  ( ph  <->  th )

Proof of Theorem 3bitr2i
StepHypRef Expression
1 3bitr2i.1 . . 3  |-  ( ph  <->  ps )
2 3bitr2i.2 . . 3  |-  ( ch  <->  ps )
31, 2bitr4i 185 . 2  |-  ( ph  <->  ch )
4 3bitr2i.3 . 2  |-  ( ch  <->  th )
53, 4bitri 182 1  |-  ( ph  <->  th )
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  1811  sbexyz  1921  exists1  2038  euxfrdc  2779  euind  2780  rmo4  2786  rmo3  2906  ddifstab  3105  opm  3997  uniuni  4209  rabxp  4406  eliunxp  4503  dmmrnm  4582  imadisj  4717  intirr  4741  resco  4855  funcnv3  4992  fncnv  4996  fun11  4997  fununi  4998  f1mpt  5442  mpt2mptx  5626  xpcomco  6370  enq0tr  6686  elq  8788
  Copyright terms: Public domain W3C validator