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

Theorem 3bitr4ri 211
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 185 . 2  |-  ( ph  <->  th )
51, 4bitr2i 183 1  |-  ( th  <->  ch )
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:  testbitestn  857  excxor  1310  sbequ8  1769  2sb5  1901  2sb6  1902  2sb5rf  1907  2sb6rf  1908  moabs  1991  moanim  2016  2eu4  2035  2eu7  2036  sb8ab  2201  risset  2395  reuind  2796  difundi  3223  indifdir  3227  unab  3238  inab  3239  rabeq0  3281  abeq0  3282  inssdif0im  3318  snprc  3465  snss  3524  unipr  3623  uni0b  3634  pwtr  3982  opm  3997  onintexmid  4323  elxp2  4389  opthprc  4417  xpiundir  4425  elvvv  4429  relun  4482  inopab  4496  difopab  4497  ralxpf  4510  rexxpf  4511  dmiun  4572  rniun  4764  cnvresima  4840  imaco  4856  fnopabg  5053  dff1o2  5162  idref  5428  imaiun  5431  opabex3d  5779  opabex3  5780  elixx3g  9000  elfz2  9112  elfzuzb  9115  divalgb  10469  1nprm  10640  alsconv  10949
  Copyright terms: Public domain W3C validator