Theorem 3bitr3i 209

Description: A chained inference from transitive law for logical equivalence. (Contributed by NM, 19-Aug-1993.)

Hypotheses

Ref	Expression
3bitr3i.1	⊢ (𝜑 ↔ 𝜓)
3bitr3i.2	⊢ (𝜑 ↔ 𝜒)
3bitr3i.3	⊢ (𝜓 ↔ 𝜃)

Assertion

Ref	Expression
3bitr3i	⊢ (𝜒 ↔ 𝜃)

Proof of Theorem 3bitr3i

Step	Hyp	Ref	Expression
1		3bitr3i.2	. . 3 ⊢ (𝜑 ↔ 𝜒)
2		3bitr3i.1	. . 3 ⊢ (𝜑 ↔ 𝜓)
3	1, 2	bitr3i 185	. 2 ⊢ (𝜒 ↔ 𝜓)
4		3bitr3i.3	. 2 ⊢ (𝜓 ↔ 𝜃)
5	3, 4	bitri 183	1 ⊢ (𝜒 ↔ 𝜃)

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  551  cbval2  1908  cbvex2  1909  sbco2vh  1932  equsb3  1938  sbn  1939  sbim  1940  sbor  1941  sban  1942  sbco2h  1951  sbco2d  1953  sbco2vd  1954  sbcomv  1958  sbco3  1961  sbcom  1962  sbcom2v  1972  sbcom2v2  1973  sbcom2  1974  dfsb7  1978  sb7f  1979  sb7af  1980  sbal  1987  sbex  1991  sbco4lem  1993  moanim  2087  eq2tri  2224  eqsb3  2268  clelsb3  2269  clelsb4  2270  clelsb3f  2310  ralcom4  2743  rexcom4  2744  ceqsralt  2748  gencbvex  2767  gencbval  2769  ceqsrexbv  2852  euind  2908  reuind  2926  sbccomlem  3020  sbccom  3021  raaan  3510  elxp2  4616  eqbrriv  4693  dm0rn0  4815  dfres2  4930  qfto  4987  xpm  5019  rninxp  5041  fununi  5250  dfoprab2  5880  dfer2  6493  euen1  6759  xpsnen  6778  xpassen  6787  enq0enq  7363  prnmaxl  7420  prnminu  7421  suplocexprlemell  7645