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-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  an12  529  cbval2  1845  cbvex2  1846  sbco2v  1870  equsb3  1874  sbn  1875  sbim  1876  sbor  1877  sban  1878  sbco2h  1887  sbco2d  1889  sbco2vd  1890  sbcomv  1894  sbco3  1897  sbcom  1898  sbcom2v  1910  sbcom2v2  1911  sbcom2  1912  dfsb7  1916  sb7f  1917  sb7af  1918  sbal  1925  sbex  1929  sbco4lem  1931  moanim  2023  eq2tri  2148  eqsb3  2192  clelsb3  2193  clelsb4  2194  clelsb3f  2233  ralcom4  2644  rexcom4  2645  ceqsralt  2649  gencbvex  2668  gencbval  2670  ceqsrexbv  2751  euind  2805  reuind  2823  sbccomlem  2916  sbccom  2917  raaan  3394  elxp2  4472  eqbrriv  4548  dm0rn0  4668  dfres2  4779  qfto  4836  xpm  4868  rninxp  4889  fununi  5097  dfoprab2  5712  dfer2  6309  euen1  6575  xpsnen  6593  xpassen  6602  enq0enq  7053  prnmaxl  7110  prnminu  7111