Theorem 3bitr3i 210

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

Syntax hints:   ↔ wb 105

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  an12  563  cbval2  1970  cbvex2  1971  cbvaldvaw  1979  sbco2vh  1998  equsb3  2004  sbn  2005  sbim  2006  sbor  2007  sban  2008  sbco2h  2017  sbco2d  2019  sbco2vd  2020  sbcomv  2024  sbco3  2027  sbcom  2028  sbcom2v  2038  sbcom2v2  2039  sbcom2  2040  dfsb7  2044  sb7f  2045  sb7af  2046  sbal  2053  sbex  2057  sbco4lem  2059  moanim  2154  eq2tri  2291  eqsb1  2335  clelsb1  2336  clelsb2  2337  clelsb1f  2379  ralcom4  2826  rexcom4  2827  ceqsralt  2831  gencbvex  2851  gencbval  2853  ceqsrexbv  2938  euind  2994  reuind  3012  sbccomlem  3107  sbccom  3108  raaan  3602  elxp2  4749  eqbrriv  4827  dm0rn0  4954  dfres2  5071  qfto  5133  xpm  5165  rninxp  5187  fununi  5405  dfoprab2  6078  dfer2  6746  euen1  7019  xpsnen  7048  xpassen  7057  enq0enq  7694  prnmaxl  7751  prnminu  7752  suplocexprlemell  7976