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  4792  eqbrriv  4870  dm0rn0  4998  dfres2  5115  qfto  5177  xpm  5209  rninxp  5231  fununi  5449  dfoprab2  6135  dfer2  6808  euen1  7089  xpsnen  7119  xpassen  7128  enq0enq  7798  prnmaxl  7855  prnminu  7856  suplocexprlemell  8080