Theorem 3bitr3i 199

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

Syntax hints:   ↔ wb 98

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101

This theorem depends on definitions:  df-bi 110

This theorem is referenced by:  an12  495  cbval2  1796  cbvex2  1797  sbco2v  1821  equsb3  1825  sbn  1826  sbim  1827  sbor  1828  sban  1829  sbco2h  1838  sbco2d  1840  sbco2vd  1841  sbcomv  1845  sbco3  1848  sbcom  1849  sbcom2v  1861  sbcom2v2  1862  sbcom2  1863  dfsb7  1867  sb7f  1868  sb7af  1869  sbal  1876  sbex  1880  sbco4lem  1882  moanim  1974  eq2tri  2099  eqsb3  2141  clelsb3  2142  clelsb4  2143  ralcom4  2576  rexcom4  2577  ceqsralt  2581  gencbvex  2600  gencbval  2602  ceqsrexbv  2675  euind  2728  reuind  2744  sbccomlem  2832  sbccom  2833  raaan  3327  elxp2  4363  eqbrriv  4435  dm0rn0  4552  dfres2  4658  qfto  4714  xpm  4745  rninxp  4764  fununi  4967  dfoprab2  5552  dfer2  6107  euen1  6282  xpsnen  6295  xpassen  6304  enq0enq  6529  prnmaxl  6586  prnminu  6587