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  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