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  1945  cbvex2  1946  cbvaldvaw  1954  sbco2vh  1973  equsb3  1979  sbn  1980  sbim  1981  sbor  1982  sban  1983  sbco2h  1992  sbco2d  1994  sbco2vd  1995  sbcomv  1999  sbco3  2002  sbcom  2003  sbcom2v  2013  sbcom2v2  2014  sbcom2  2015  dfsb7  2019  sb7f  2020  sb7af  2021  sbal  2028  sbex  2032  sbco4lem  2034  moanim  2128  eq2tri  2265  eqsb1  2309  clelsb1  2310  clelsb2  2311  clelsb1f  2352  ralcom4  2794  rexcom4  2795  ceqsralt  2799  gencbvex  2819  gencbval  2821  ceqsrexbv  2904  euind  2960  reuind  2978  sbccomlem  3073  sbccom  3074  raaan  3566  elxp2  4693  eqbrriv  4770  dm0rn0  4895  dfres2  5011  qfto  5072  xpm  5104  rninxp  5126  fununi  5342  dfoprab2  5992  dfer2  6621  euen1  6894  xpsnen  6916  xpassen  6925  enq0enq  7544  prnmaxl  7601  prnminu  7602  suplocexprlemell  7826