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

Theorem 3bitr3i 208
Description: A chained inference from transitive law for logical equivalence. (Contributed by NM, 19-Aug-1993.)
Hypotheses
Ref Expression
3bitr3i.1  |-  ( ph  <->  ps )
3bitr3i.2  |-  ( ph  <->  ch )
3bitr3i.3  |-  ( ps  <->  th )
Assertion
Ref Expression
3bitr3i  |-  ( ch  <->  th )

Proof of Theorem 3bitr3i
StepHypRef Expression
1 3bitr3i.2 . . 3  |-  ( ph  <->  ch )
2 3bitr3i.1 . . 3  |-  ( ph  <->  ps )
31, 2bitr3i 184 . 2  |-  ( ch  <->  ps )
4 3bitr3i.3 . 2  |-  ( ps  <->  th )
53, 4bitri 182 1  |-  ( ch  <->  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:  an12  526  cbval2  1838  cbvex2  1839  sbco2v  1863  equsb3  1867  sbn  1868  sbim  1869  sbor  1870  sban  1871  sbco2h  1880  sbco2d  1882  sbco2vd  1883  sbcomv  1887  sbco3  1890  sbcom  1891  sbcom2v  1903  sbcom2v2  1904  sbcom2  1905  dfsb7  1909  sb7f  1910  sb7af  1911  sbal  1918  sbex  1922  sbco4lem  1924  moanim  2016  eq2tri  2141  eqsb3  2183  clelsb3  2184  clelsb4  2185  ralcom4  2622  rexcom4  2623  ceqsralt  2627  gencbvex  2646  gencbval  2648  ceqsrexbv  2727  euind  2780  reuind  2796  sbccomlem  2889  sbccom  2890  raaan  3355  elxp2  4389  eqbrriv  4461  dm0rn0  4580  dfres2  4688  qfto  4744  xpm  4775  rninxp  4794  fununi  4998  dfoprab2  5583  dfer2  6173  euen1  6349  xpsnen  6365  xpassen  6374  enq0enq  6683  prnmaxl  6740  prnminu  6741
  Copyright terms: Public domain W3C validator