Theorem 3bitr3i 203

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

Syntax hints:   ↔ wb 102

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 103  ax-ia2 104  ax-ia3 105

This theorem depends on definitions:  df-bi 114

This theorem is referenced by:  an12  503  cbval2  1812  cbvex2  1813  sbco2v  1837  equsb3  1841  sbn  1842  sbim  1843  sbor  1844  sban  1845  sbco2h  1854  sbco2d  1856  sbco2vd  1857  sbcomv  1861  sbco3  1864  sbcom  1865  sbcom2v  1877  sbcom2v2  1878  sbcom2  1879  dfsb7  1883  sb7f  1884  sb7af  1885  sbal  1892  sbex  1896  sbco4lem  1898  moanim  1990  eq2tri  2115  eqsb3  2157  clelsb3  2158  clelsb4  2159  ralcom4  2593  rexcom4  2594  ceqsralt  2598  gencbvex  2617  gencbval  2619  ceqsrexbv  2697  euind  2750  reuind  2766  sbccomlem  2859  sbccom  2860  raaan  3354  elxp2  4390  eqbrriv  4462  dm0rn0  4579  dfres2  4685  qfto  4741  xpm  4772  rninxp  4791  fununi  4994  dfoprab2  5579  dfer2  6137  euen1  6312  xpsnen  6325  xpassen  6334  enq0enq  6586  prnmaxl  6643  prnminu  6644