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

Step	Hyp	Ref	Expression
1		3bitr3i.2	. . 3 |- ( ph <-> ch )
2		3bitr3i.1	. . 3 |- ( ph <-> ps )
3	1, 2	bitr3i 185	. 2 |- ( ch <-> ps )
4		3bitr3i.3	. 2 |- ( ps <-> th )
5	3, 4	bitri 183	1 |- ( ch <-> th )

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  1894  cbvex2  1895  sbco2vh  1919  equsb3  1925  sbn  1926  sbim  1927  sbor  1928  sban  1929  sbco2h  1938  sbco2d  1940  sbco2vd  1941  sbcomv  1945  sbco3  1948  sbcom  1949  sbcom2v  1961  sbcom2v2  1962  sbcom2  1963  dfsb7  1967  sb7f  1968  sb7af  1969  sbal  1976  sbex  1980  sbco4lem  1982  moanim  2074  eq2tri  2200  eqsb3  2244  clelsb3  2245  clelsb4  2246  clelsb3f  2286  ralcom4  2711  rexcom4  2712  ceqsralt  2716  gencbvex  2735  gencbval  2737  ceqsrexbv  2820  euind  2875  reuind  2893  sbccomlem  2987  sbccom  2988  raaan  3474  elxp2  4565  eqbrriv  4642  dm0rn0  4764  dfres2  4879  qfto  4936  xpm  4968  rninxp  4990  fununi  5199  dfoprab2  5826  dfer2  6438  euen1  6704  xpsnen  6723  xpassen  6732  enq0enq  7263  prnmaxl  7320  prnminu  7321  suplocexprlemell  7545