Theorem 3bitr3i 208

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 184	. 2 ⊢ (𝜒 ↔ 𝜓)
4		3bitr3i.3	. 2 ⊢ (𝜓 ↔ 𝜃)
5	3, 4	bitri 182	1 ⊢ (𝜒 ↔ 𝜃)

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  526  cbval2  1841  cbvex2  1842  sbco2v  1866  equsb3  1870  sbn  1871  sbim  1872  sbor  1873  sban  1874  sbco2h  1883  sbco2d  1885  sbco2vd  1886  sbcomv  1890  sbco3  1893  sbcom  1894  sbcom2v  1906  sbcom2v2  1907  sbcom2  1908  dfsb7  1912  sb7f  1913  sb7af  1914  sbal  1921  sbex  1925  sbco4lem  1927  moanim  2019  eq2tri  2144  eqsb3  2188  clelsb3  2189  clelsb4  2190  ralcom4  2635  rexcom4  2636  ceqsralt  2640  gencbvex  2659  gencbval  2661  ceqsrexbv  2739  euind  2793  reuind  2809  sbccomlem  2902  sbccom  2903  raaan  3375  elxp2  4427  eqbrriv  4499  dm0rn0  4619  dfres2  4727  qfto  4784  xpm  4815  rninxp  4836  fununi  5043  dfoprab2  5646  dfer2  6238  euen1  6464  xpsnen  6482  xpassen  6491  enq0enq  6926  prnmaxl  6983  prnminu  6984