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  1968  cbvex2  1969  cbvaldvaw  1977  sbco2vh  1996  equsb3  2002  sbn  2003  sbim  2004  sbor  2005  sban  2006  sbco2h  2015  sbco2d  2017  sbco2vd  2018  sbcomv  2022  sbco3  2025  sbcom  2026  sbcom2v  2036  sbcom2v2  2037  sbcom2  2038  dfsb7  2042  sb7f  2043  sb7af  2044  sbal  2051  sbex  2055  sbco4lem  2057  moanim  2152  eq2tri  2289  eqsb1  2333  clelsb1  2334  clelsb2  2335  clelsb1f  2376  ralcom4  2823  rexcom4  2824  ceqsralt  2828  gencbvex  2848  gencbval  2850  ceqsrexbv  2935  euind  2991  reuind  3009  sbccomlem  3104  sbccom  3105  raaan  3598  elxp2  4741  eqbrriv  4819  dm0rn0  4946  dfres2  5063  qfto  5124  xpm  5156  rninxp  5178  fununi  5395  dfoprab2  6063  dfer2  6698  euen1  6971  xpsnen  7000  xpassen  7009  enq0enq  7641  prnmaxl  7698  prnminu  7699  suplocexprlemell  7923