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  1968  cbvex2  1969  cbvaldvaw  1977  sbco2vh  1996  equsb3  2002  sbn  2003  sbim  2004  sbor  2005  sban  2006  sbco2h  2015  sbco2d  2017  sbco2vd  2018  sbcomv  2022  sbco3  2025  sbcom  2026  sbcom2v  2036  sbcom2v2  2037  sbcom2  2038  dfsb7  2042  sb7f  2043  sb7af  2044  sbal  2051  sbex  2055  sbco4lem  2057  moanim  2152  eq2tri  2289  eqsb1  2333  clelsb1  2334  clelsb2  2335  clelsb1f  2376  ralcom4  2822  rexcom4  2823  ceqsralt  2827  gencbvex  2847  gencbval  2849  ceqsrexbv  2934  euind  2990  reuind  3008  sbccomlem  3103  sbccom  3104  raaan  3597  elxp2  4734  eqbrriv  4811  dm0rn0  4937  dfres2  5053  qfto  5114  xpm  5146  rninxp  5168  fununi  5385  dfoprab2  6042  dfer2  6671  euen1  6944  xpsnen  6968  xpassen  6977  enq0enq  7606  prnmaxl  7663  prnminu  7664  suplocexprlemell  7888