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  2923  euind  2924  rmo4  2930  rmo3f  2934  rmo3  3054  ddifstab  3267  opm  4234  uniuni  4451  rabxp  4663  eliunxp  4766  dmmrnm  4846  imadisj  4990  intirr  5015  resco  5133  funcnv3  5278  fncnv  5282  fun11  5283  fununi  5284  f1mpt  5771  mpomptx  5965  ixp0x  6725  mapsnen  6810  xpcomco  6825  enq0tr  7432  elq  9620  pythagtrip  12277  ntreq0  13563  tx1cn  13700
  Copyright terms: Public domain W3C validator