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

Theorem 3bitr2i 208
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 187 . 2  |-  ( ph  <->  ch )
4 3bitr2i.3 . 2  |-  ( ch  <->  th )
53, 4bitri 184 1  |-  ( ph  <->  th )
Colors of variables: wff set class
Syntax hints:    <-> wb 105
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108
This theorem depends on definitions:  df-bi 117
This theorem is referenced by:  an13  563  sbanv  1889  sbexyz  2003  exists1  2122  euxfrdc  2925  euind  2926  rmo4  2932  rmo3f  2936  rmo3  3056  ddifstab  3269  opm  4236  uniuni  4453  rabxp  4665  eliunxp  4768  dmmrnm  4848  imadisj  4992  intirr  5017  resco  5135  funcnv3  5280  fncnv  5284  fun11  5285  fununi  5286  f1mpt  5774  mpomptx  5968  ixp0x  6728  mapsnen  6813  xpcomco  6828  enq0tr  7435  elq  9624  pythagtrip  12285  ntreq0  13671  tx1cn  13808
  Copyright terms: Public domain W3C validator