Theorem 3bitr3i 210

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 186	. 2 |- ( ch <-> ps )
4		3bitr3i.3	. 2 |- ( ps <-> th )
5	3, 4	bitri 184	1 |- ( ch <-> th )

Syntax hints:   <-> wb 105

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  an12  561  cbval2  1946  cbvex2  1947  cbvaldvaw  1955  sbco2vh  1974  equsb3  1980  sbn  1981  sbim  1982  sbor  1983  sban  1984  sbco2h  1993  sbco2d  1995  sbco2vd  1996  sbcomv  2000  sbco3  2003  sbcom  2004  sbcom2v  2014  sbcom2v2  2015  sbcom2  2016  dfsb7  2020  sb7f  2021  sb7af  2022  sbal  2029  sbex  2033  sbco4lem  2035  moanim  2130  eq2tri  2267  eqsb1  2311  clelsb1  2312  clelsb2  2313  clelsb1f  2354  ralcom4  2799  rexcom4  2800  ceqsralt  2804  gencbvex  2824  gencbval  2826  ceqsrexbv  2911  euind  2967  reuind  2985  sbccomlem  3080  sbccom  3081  raaan  3574  elxp2  4711  eqbrriv  4788  dm0rn0  4914  dfres2  5030  qfto  5091  xpm  5123  rninxp  5145  fununi  5361  dfoprab2  6015  dfer2  6644  euen1  6917  xpsnen  6941  xpassen  6950  enq0enq  7579  prnmaxl  7636  prnminu  7637  suplocexprlemell  7861