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

Theorem 3bitr4ri 213
Description: A chained inference from transitive law for logical equivalence. (Contributed by NM, 2-Sep-1995.)
Hypotheses
Ref Expression
3bitr4i.1  |-  ( ph  <->  ps )
3bitr4i.2  |-  ( ch  <->  ph )
3bitr4i.3  |-  ( th  <->  ps )
Assertion
Ref Expression
3bitr4ri  |-  ( th  <->  ch )

Proof of Theorem 3bitr4ri
StepHypRef Expression
1 3bitr4i.2 . 2  |-  ( ch  <->  ph )
2 3bitr4i.1 . . 3  |-  ( ph  <->  ps )
3 3bitr4i.3 . . 3  |-  ( th  <->  ps )
42, 3bitr4i 187 . 2  |-  ( ph  <->  th )
51, 4bitr2i 185 1  |-  ( th  <->  ch )
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:  dcnnOLD  851  excxor  1398  sbequ8  1870  2sb5  2011  2sb6  2012  2sb5rf  2017  2sb6rf  2018  moabs  2103  moanim  2128  2eu4  2147  2eu7  2148  sb8ab  2327  risset  2534  cbvreuvw  2744  reuind  2978  difundi  3425  indifdir  3429  unab  3440  inab  3441  rabeq0  3490  abeq0  3491  inssdif0im  3528  snprc  3698  snssOLD  3759  unipr  3864  uni0b  3875  pwtr  4263  opm  4278  onintexmid  4621  elxp2  4693  opthprc  4726  xpiundir  4734  elvvv  4738  relun  4792  inopab  4810  difopab  4811  ralxpf  4824  rexxpf  4825  dmiun  4887  rniun  5093  cnvresima  5172  imaco  5188  fnopabg  5399  dff1o2  5527  idref  5825  imaiun  5829  opabex3d  6206  opabex3  6207  onntri35  7349  elixx3g  10023  elfz2  10137  elfzuzb  10141  divalgb  12236  1nprm  12436  issubg3  13528  cnfldui  14351  alsconv  16019
  Copyright terms: Public domain W3C validator