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  1933  cbvex2  1934  cbvaldvaw  1942  sbco2vh  1961  equsb3  1967  sbn  1968  sbim  1969  sbor  1970  sban  1971  sbco2h  1980  sbco2d  1982  sbco2vd  1983  sbcomv  1987  sbco3  1990  sbcom  1991  sbcom2v  2001  sbcom2v2  2002  sbcom2  2003  dfsb7  2007  sb7f  2008  sb7af  2009  sbal  2016  sbex  2020  sbco4lem  2022  moanim  2116  eq2tri  2253  eqsb1  2297  clelsb1  2298  clelsb2  2299  clelsb1f  2340  ralcom4  2782  rexcom4  2783  ceqsralt  2787  gencbvex  2806  gencbval  2808  ceqsrexbv  2891  euind  2947  reuind  2965  sbccomlem  3060  sbccom  3061  raaan  3552  elxp2  4677  eqbrriv  4754  dm0rn0  4879  dfres2  4994  qfto  5055  xpm  5087  rninxp  5109  fununi  5322  dfoprab2  5965  dfer2  6588  euen1  6856  xpsnen  6875  xpassen  6884  enq0enq  7491  prnmaxl  7548  prnminu  7549  suplocexprlemell  7773