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  561  cbval2  1946  cbvex2  1947  cbvaldvaw  1955  sbco2vh  1974  equsb3  1980  sbn  1981  sbim  1982  sbor  1983  sban  1984  sbco2h  1993  sbco2d  1995  sbco2vd  1996  sbcomv  2000  sbco3  2003  sbcom  2004  sbcom2v  2014  sbcom2v2  2015  sbcom2  2016  dfsb7  2020  sb7f  2021  sb7af  2022  sbal  2029  sbex  2033  sbco4lem  2035  moanim  2129  eq2tri  2266  eqsb1  2310  clelsb1  2311  clelsb2  2312  clelsb1f  2353  ralcom4  2796  rexcom4  2797  ceqsralt  2801  gencbvex  2821  gencbval  2823  ceqsrexbv  2906  euind  2962  reuind  2980  sbccomlem  3075  sbccom  3076  raaan  3568  elxp2  4698  eqbrriv  4775  dm0rn0  4901  dfres2  5017  qfto  5078  xpm  5110  rninxp  5132  fununi  5348  dfoprab2  6002  dfer2  6631  euen1  6904  xpsnen  6928  xpassen  6937  enq0enq  7557  prnmaxl  7614  prnminu  7615  suplocexprlemell  7839