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

Theorem 3bitr3i 209
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 185 . 2  |-  ( ch  <->  ps )
4 3bitr3i.3 . 2  |-  ( ps  <->  th )
53, 4bitri 183 1  |-  ( ch  <->  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:  an12  551  cbval2  1901  cbvex2  1902  sbco2vh  1925  equsb3  1931  sbn  1932  sbim  1933  sbor  1934  sban  1935  sbco2h  1944  sbco2d  1946  sbco2vd  1947  sbcomv  1951  sbco3  1954  sbcom  1955  sbcom2v  1965  sbcom2v2  1966  sbcom2  1967  dfsb7  1971  sb7f  1972  sb7af  1973  sbal  1980  sbex  1984  sbco4lem  1986  moanim  2080  eq2tri  2217  eqsb3  2261  clelsb3  2262  clelsb4  2263  clelsb3f  2303  ralcom4  2734  rexcom4  2735  ceqsralt  2739  gencbvex  2758  gencbval  2760  ceqsrexbv  2843  euind  2899  reuind  2917  sbccomlem  3011  sbccom  3012  raaan  3500  elxp2  4604  eqbrriv  4681  dm0rn0  4803  dfres2  4918  qfto  4975  xpm  5007  rninxp  5029  fununi  5238  dfoprab2  5868  dfer2  6481  euen1  6747  xpsnen  6766  xpassen  6775  enq0enq  7351  prnmaxl  7408  prnminu  7409  suplocexprlemell  7633
  Copyright terms: Public domain W3C validator