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  556  cbval2  1914  cbvex2  1915  sbco2vh  1938  equsb3  1944  sbn  1945  sbim  1946  sbor  1947  sban  1948  sbco2h  1957  sbco2d  1959  sbco2vd  1960  sbcomv  1964  sbco3  1967  sbcom  1968  sbcom2v  1978  sbcom2v2  1979  sbcom2  1980  dfsb7  1984  sb7f  1985  sb7af  1986  sbal  1993  sbex  1997  sbco4lem  1999  moanim  2093  eq2tri  2230  eqsb1  2274  clelsb1  2275  clelsb2  2276  clelsb1f  2316  ralcom4  2752  rexcom4  2753  ceqsralt  2757  gencbvex  2776  gencbval  2778  ceqsrexbv  2861  euind  2917  reuind  2935  sbccomlem  3029  sbccom  3030  raaan  3521  elxp2  4629  eqbrriv  4706  dm0rn0  4828  dfres2  4943  qfto  5000  xpm  5032  rninxp  5054  fununi  5266  dfoprab2  5900  dfer2  6514  euen1  6780  xpsnen  6799  xpassen  6808  enq0enq  7393  prnmaxl  7450  prnminu  7451  suplocexprlemell  7675