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

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  an12  551  cbval2  1909  cbvex2  1910  sbco2vh  1933  equsb3  1939  sbn  1940  sbim  1941  sbor  1942  sban  1943  sbco2h  1952  sbco2d  1954  sbco2vd  1955  sbcomv  1959  sbco3  1962  sbcom  1963  sbcom2v  1973  sbcom2v2  1974  sbcom2  1975  dfsb7  1979  sb7f  1980  sb7af  1981  sbal  1988  sbex  1992  sbco4lem  1994  moanim  2088  eq2tri  2226  eqsb1  2270  clelsb1  2271  clelsb2  2272  clelsb1f  2312  ralcom4  2748  rexcom4  2749  ceqsralt  2753  gencbvex  2772  gencbval  2774  ceqsrexbv  2857  euind  2913  reuind  2931  sbccomlem  3025  sbccom  3026  raaan  3515  elxp2  4622  eqbrriv  4699  dm0rn0  4821  dfres2  4936  qfto  4993  xpm  5025  rninxp  5047  fununi  5256  dfoprab2  5889  dfer2  6502  euen1  6768  xpsnen  6787  xpassen  6796  enq0enq  7372  prnmaxl  7429  prnminu  7430  suplocexprlemell  7654