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-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  an12  533  cbval2  1869  cbvex2  1870  sbco2v  1894  equsb3  1898  sbn  1899  sbim  1900  sbor  1901  sban  1902  sbco2h  1911  sbco2d  1913  sbco2vd  1914  sbcomv  1918  sbco3  1921  sbcom  1922  sbcom2v  1934  sbcom2v2  1935  sbcom2  1936  dfsb7  1940  sb7f  1941  sb7af  1942  sbal  1949  sbex  1953  sbco4lem  1955  moanim  2047  eq2tri  2172  eqsb3  2216  clelsb3  2217  clelsb4  2218  clelsb3f  2257  ralcom4  2677  rexcom4  2678  ceqsralt  2682  gencbvex  2701  gencbval  2703  ceqsrexbv  2784  euind  2838  reuind  2856  sbccomlem  2949  sbccom  2950  raaan  3433  elxp2  4515  eqbrriv  4592  dm0rn0  4714  dfres2  4827  qfto  4884  xpm  4916  rninxp  4938  fununi  5147  dfoprab2  5770  dfer2  6381  euen1  6647  xpsnen  6665  xpassen  6674  enq0enq  7180  prnmaxl  7237  prnminu  7238