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  1936  cbvex2  1937  cbvaldvaw  1945  sbco2vh  1964  equsb3  1970  sbn  1971  sbim  1972  sbor  1973  sban  1974  sbco2h  1983  sbco2d  1985  sbco2vd  1986  sbcomv  1990  sbco3  1993  sbcom  1994  sbcom2v  2004  sbcom2v2  2005  sbcom2  2006  dfsb7  2010  sb7f  2011  sb7af  2012  sbal  2019  sbex  2023  sbco4lem  2025  moanim  2119  eq2tri  2256  eqsb1  2300  clelsb1  2301  clelsb2  2302  clelsb1f  2343  ralcom4  2785  rexcom4  2786  ceqsralt  2790  gencbvex  2810  gencbval  2812  ceqsrexbv  2895  euind  2951  reuind  2969  sbccomlem  3064  sbccom  3065  raaan  3557  elxp2  4682  eqbrriv  4759  dm0rn0  4884  dfres2  4999  qfto  5060  xpm  5092  rninxp  5114  fununi  5327  dfoprab2  5973  dfer2  6602  euen1  6870  xpsnen  6889  xpassen  6898  enq0enq  7515  prnmaxl  7572  prnminu  7573  suplocexprlemell  7797