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  1970  cbvex2  1971  cbvaldvaw  1979  sbco2vh  1998  equsb3  2004  sbn  2005  sbim  2006  sbor  2007  sban  2008  sbco2h  2017  sbco2d  2019  sbco2vd  2020  sbcomv  2024  sbco3  2027  sbcom  2028  sbcom2v  2038  sbcom2v2  2039  sbcom2  2040  dfsb7  2044  sb7f  2045  sb7af  2046  sbal  2053  sbex  2057  sbco4lem  2059  moanim  2154  eq2tri  2291  eqsb1  2335  clelsb1  2336  clelsb2  2337  clelsb1f  2378  ralcom4  2825  rexcom4  2826  ceqsralt  2830  gencbvex  2850  gencbval  2852  ceqsrexbv  2937  euind  2993  reuind  3011  sbccomlem  3106  sbccom  3107  raaan  3600  elxp2  4743  eqbrriv  4821  dm0rn0  4948  dfres2  5065  qfto  5126  xpm  5158  rninxp  5180  fununi  5398  dfoprab2  6067  dfer2  6702  euen1  6975  xpsnen  7004  xpassen  7013  enq0enq  7650  prnmaxl  7707  prnminu  7708  suplocexprlemell  7932