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

Theorem 3bitr2i 207
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 186 . 2  |-  ( ph  <->  ch )
4 3bitr2i.3 . 2  |-  ( ch  <->  th )
53, 4bitri 183 1  |-  ( ph  <->  th )
Colors of variables: wff set class
Syntax hints:    <-> wb 104
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107
This theorem depends on definitions:  df-bi 116
This theorem is referenced by:  an13  537  sbanv  1845  sbexyz  1956  exists1  2073  euxfrdc  2843  euind  2844  rmo4  2850  rmo3f  2854  rmo3  2972  ddifstab  3178  opm  4126  uniuni  4342  rabxp  4546  eliunxp  4648  dmmrnm  4728  imadisj  4871  intirr  4895  resco  5013  funcnv3  5155  fncnv  5159  fun11  5160  fununi  5161  f1mpt  5640  mpomptx  5830  ixp0x  6588  mapsnen  6673  xpcomco  6688  enq0tr  7210  elq  9382  ntreq0  12228  tx1cn  12365
  Copyright terms: Public domain W3C validator