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  1839  cbvex2  1840  sbco2v  1864  equsb3  1868  sbn  1869  sbim  1870  sbor  1871  sban  1872  sbco2h  1881  sbco2d  1883  sbco2vd  1884  sbcomv  1888  sbco3  1891  sbcom  1892  sbcom2v  1904  sbcom2v2  1905  sbcom2  1906  dfsb7  1910  sb7f  1911  sb7af  1912  sbal  1919  sbex  1923  sbco4lem  1925  moanim  2017  eq2tri  2142  eqsb3  2186  clelsb3  2187  clelsb4  2188  ralcom4  2631  rexcom4  2632  ceqsralt  2636  gencbvex  2655  gencbval  2657  ceqsrexbv  2735  euind  2789  reuind  2805  sbccomlem  2898  sbccom  2899  raaan  3365  elxp2  4410  eqbrriv  4482  dm0rn0  4601  dfres2  4709  qfto  4765  xpm  4796  rninxp  4815  fununi  5019  dfoprab2  5605  dfer2  6196  euen1  6372  xpsnen  6388  xpassen  6397  enq0enq  6760  prnmaxl  6817  prnminu  6818