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  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  3630  elxp2  4787  eqbrriv  4865  dm0rn0  4993  dfres2  5110  qfto  5172  xpm  5204  rninxp  5226  fununi  5444  dfoprab2  6125  dfer2  6798  euen1  7079  xpsnen  7109  xpassen  7118  enq0enq  7788  prnmaxl  7845  prnminu  7846  suplocexprlemell  8070