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  1921  cbvex2  1922  sbco2vh  1945  equsb3  1951  sbn  1952  sbim  1953  sbor  1954  sban  1955  sbco2h  1964  sbco2d  1966  sbco2vd  1967  sbcomv  1971  sbco3  1974  sbcom  1975  sbcom2v  1985  sbcom2v2  1986  sbcom2  1987  dfsb7  1991  sb7f  1992  sb7af  1993  sbal  2000  sbex  2004  sbco4lem  2006  moanim  2100  eq2tri  2237  eqsb1  2281  clelsb1  2282  clelsb2  2283  clelsb1f  2323  ralcom4  2761  rexcom4  2762  ceqsralt  2766  gencbvex  2785  gencbval  2787  ceqsrexbv  2870  euind  2926  reuind  2944  sbccomlem  3039  sbccom  3040  raaan  3531  elxp2  4646  eqbrriv  4723  dm0rn0  4846  dfres2  4961  qfto  5020  xpm  5052  rninxp  5074  fununi  5286  dfoprab2  5925  dfer2  6539  euen1  6805  xpsnen  6824  xpassen  6833  enq0enq  7433  prnmaxl  7490  prnminu  7491  suplocexprlemell  7715