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 )

This proof depends on syntax axioms:   <-> wb 105

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This proof depends on definitions:  df-bi 117

This theorem is used by:  an12  567  cbval2  1977  cbvex2  1978  cbvaldvaw  1986  sbco2vh  2005  equsb3  2011  sbn  2012  sbim  2013  sbor  2014  sban  2015  sbco2h  2024  sbco2d  2026  sbco2vd  2027  sbcomv  2031  sbco3  2034  sbcom  2035  sbcom2v  2045  sbcom2v2  2046  sbcom2  2047  dfsb7  2051  sb7f  2052  sb7af  2053  sbal  2060  sbex  2064  sbco4lem  2066  moanim  2161  eq2tri  2298  eqsb1  2342  clelsb1  2343  clelsb2  2344  clelsb1f  2396  ralcom4  2844  rexcom4  2845  ceqsralt  2849  gencbvex  2869  gencbval  2871  ceqsrexbv  2957  euind  3013  reuind  3031  sbccomlem  3126  sbccom  3127  raaan  3633  elxp2  4794  eqbrriv  4872  dm0rn0  5000  dfres2  5118  qfto  5180  xpm  5212  rninxp  5234  fununi  5452  dfoprab2  6138  dfer2  6812  euen1  7093  xpsnen  7123  xpassen  7132  enq0enq  7804  prnmaxl  7861  prnminu  7862  suplocexprlemell  8086