Theorem 3bitr3i 208

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 184	. 2 |- ( ch <-> ps )
4		3bitr3i.3	. 2 |- ( ps <-> th )
5	3, 4	bitri 182	1 |- ( ch <-> th )

Syntax hints:   <-> wb 103

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106

This theorem depends on definitions:  df-bi 115

This theorem is referenced by:  an12  525  cbval2  1837  cbvex2  1838  sbco2v  1862  equsb3  1866  sbn  1867  sbim  1868  sbor  1869  sban  1870  sbco2h  1879  sbco2d  1881  sbco2vd  1882  sbcomv  1886  sbco3  1889  sbcom  1890  sbcom2v  1902  sbcom2v2  1903  sbcom2  1904  dfsb7  1908  sb7f  1909  sb7af  1910  sbal  1917  sbex  1921  sbco4lem  1923  moanim  2015  eq2tri  2140  eqsb3  2182  clelsb3  2183  clelsb4  2184  ralcom4  2621  rexcom4  2622  ceqsralt  2626  gencbvex  2645  gencbval  2647  ceqsrexbv  2726  euind  2779  reuind  2795  sbccomlem  2888  sbccom  2889  raaan  3347  elxp2  4381  eqbrriv  4453  dm0rn0  4570  dfres2  4678  qfto  4734  xpm  4765  rninxp  4784  fununi  4987  dfoprab2  5572  dfer2  6130  euen1  6305  xpsnen  6318  xpassen  6327  enq0enq  6621  prnmaxl  6678  prnminu  6679