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  1973  cbvex2  1974  cbvaldvaw  1982  sbco2vh  2001  equsb3  2007  sbn  2008  sbim  2009  sbor  2010  sban  2011  sbco2h  2020  sbco2d  2022  sbco2vd  2023  sbcomv  2027  sbco3  2030  sbcom  2031  sbcom2v  2041  sbcom2v2  2042  sbcom2  2043  dfsb7  2047  sb7f  2048  sb7af  2049  sbal  2056  sbex  2060  sbco4lem  2062  moanim  2157  eq2tri  2294  eqsb1  2338  clelsb1  2339  clelsb2  2340  clelsb1f  2390  ralcom4  2838  rexcom4  2839  ceqsralt  2843  gencbvex  2863  gencbval  2865  ceqsrexbv  2951  euind  3007  reuind  3025  sbccomlem  3120  sbccom  3121  raaan  3619  elxp2  4772  eqbrriv  4850  dm0rn0  4978  dfres2  5095  qfto  5157  xpm  5189  rninxp  5211  fununi  5429  dfoprab2  6108  dfer2  6781  euen1  7055  xpsnen  7085  xpassen  7094  enq0enq  7762  prnmaxl  7819  prnminu  7820  suplocexprlemell  8044