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  530  sbanv  1817  sbexyz  1927  exists1  2044  euxfrdc  2799  euind  2800  rmo4  2806  rmo3f  2810  rmo3  2928  ddifstab  3130  opm  4052  uniuni  4264  rabxp  4463  eliunxp  4563  dmmrnm  4643  imadisj  4781  intirr  4805  resco  4922  funcnv3  5062  fncnv  5066  fun11  5067  fununi  5068  f1mpt  5532  mpt2mptx  5721  mapsnen  6508  xpcomco  6522  enq0tr  6972  elq  9076
  Copyright terms: Public domain W3C validator