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  563  cbval2  1973  cbvex2  1974  cbvaldvaw  1982  sbco2vh  2001  equsb3  2007  sbn  2008  sbim  2009  sbor  2010  sban  2011  sbco2h  2020  sbco2d  2022  sbco2vd  2023  sbcomv  2027  sbco3  2030  sbcom  2031  sbcom2v  2041  sbcom2v2  2042  sbcom2  2043  dfsb7  2047  sb7f  2048  sb7af  2049  sbal  2056  sbex  2060  sbco4lem  2062  moanim  2157  eq2tri  2294  eqsb1  2338  clelsb1  2339  clelsb2  2340  clelsb1f  2390  ralcom4  2838  rexcom4  2839  ceqsralt  2843  gencbvex  2863  gencbval  2865  ceqsrexbv  2950  euind  3006  reuind  3024  sbccomlem  3119  sbccom  3120  raaan  3617  elxp2  4769  eqbrriv  4847  dm0rn0  4975  dfres2  5092  qfto  5154  xpm  5186  rninxp  5208  fununi  5426  dfoprab2  6102  dfer2  6770  euen1  7044  xpsnen  7074  xpassen  7083  enq0enq  7748  prnmaxl  7805  prnminu  7806  suplocexprlemell  8030