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  550  cbval2  1891  cbvex2  1892  sbco2vh  1916  equsb3  1922  sbn  1923  sbim  1924  sbor  1925  sban  1926  sbco2h  1935  sbco2d  1937  sbco2vd  1938  sbcomv  1942  sbco3  1945  sbcom  1946  sbcom2v  1958  sbcom2v2  1959  sbcom2  1960  dfsb7  1964  sb7f  1965  sb7af  1966  sbal  1973  sbex  1977  sbco4lem  1979  moanim  2071  eq2tri  2197  eqsb3  2241  clelsb3  2242  clelsb4  2243  clelsb3f  2283  ralcom4  2703  rexcom4  2704  ceqsralt  2708  gencbvex  2727  gencbval  2729  ceqsrexbv  2811  euind  2866  reuind  2884  sbccomlem  2978  sbccom  2979  raaan  3464  elxp2  4552  eqbrriv  4629  dm0rn0  4751  dfres2  4866  qfto  4923  xpm  4955  rninxp  4977  fununi  5186  dfoprab2  5811  dfer2  6423  euen1  6689  xpsnen  6708  xpassen  6717  enq0enq  7232  prnmaxl  7289  prnminu  7290  suplocexprlemell  7514