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  861  excxor  1314  sbequ8  1775  2sb5  1907  2sb6  1908  2sb5rf  1913  2sb6rf  1914  moabs  1997  moanim  2022  2eu4  2041  2eu7  2042  sb8ab  2209  risset  2406  reuind  2818  difundi  3249  indifdir  3253  unab  3264  inab  3265  rabeq0  3310  abeq0  3311  inssdif0im  3347  snprc  3502  snss  3561  unipr  3662  uni0b  3673  pwtr  4037  opm  4052  onintexmid  4378  elxp2  4446  opthprc  4477  xpiundir  4485  elvvv  4489  relun  4542  inopab  4556  difopab  4557  ralxpf  4570  rexxpf  4571  dmiun  4633  rniun  4829  cnvresima  4907  imaco  4923  fnopabg  5123  dff1o2  5242  idref  5518  imaiun  5521  opabex3d  5874  opabex3  5875  elixx3g  9288  elfz2  9400  elfzuzb  9403  divalgb  11018  1nprm  11189  alsconv  11580
  Copyright terms: Public domain W3C validator