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  4738  eqbrriv  4816  dm0rn0  4943  dfres2  5060  qfto  5121  xpm  5153  rninxp  5175  fununi  5392  dfoprab2  6060  dfer2  6694  euen1  6967  xpsnen  6993  xpassen  7002  enq0enq  7634  prnmaxl  7691  prnminu  7692  suplocexprlemell  7916