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  1971  cbvex2  1972  cbvaldvaw  1980  sbco2vh  1999  equsb3  2005  sbn  2006  sbim  2007  sbor  2008  sban  2009  sbco2h  2018  sbco2d  2020  sbco2vd  2021  sbcomv  2025  sbco3  2028  sbcom  2029  sbcom2v  2039  sbcom2v2  2040  sbcom2  2041  dfsb7  2045  sb7f  2046  sb7af  2047  sbal  2054  sbex  2058  sbco4lem  2060  moanim  2155  eq2tri  2292  eqsb1  2336  clelsb1  2337  clelsb2  2338  clelsb1f  2388  ralcom4  2835  rexcom4  2836  ceqsralt  2840  gencbvex  2860  gencbval  2862  ceqsrexbv  2947  euind  3003  reuind  3021  sbccomlem  3116  sbccom  3117  raaan  3614  elxp2  4766  eqbrriv  4844  dm0rn0  4972  dfres2  5089  qfto  5151  xpm  5183  rninxp  5205  fununi  5423  dfoprab2  6099  dfer2  6767  euen1  7041  xpsnen  7071  xpassen  7080  enq0enq  7745  prnmaxl  7802  prnminu  7803  suplocexprlemell  8027