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  1936  cbvex2  1937  cbvaldvaw  1945  sbco2vh  1964  equsb3  1970  sbn  1971  sbim  1972  sbor  1973  sban  1974  sbco2h  1983  sbco2d  1985  sbco2vd  1986  sbcomv  1990  sbco3  1993  sbcom  1994  sbcom2v  2004  sbcom2v2  2005  sbcom2  2006  dfsb7  2010  sb7f  2011  sb7af  2012  sbal  2019  sbex  2023  sbco4lem  2025  moanim  2119  eq2tri  2256  eqsb1  2300  clelsb1  2301  clelsb2  2302  clelsb1f  2343  ralcom4  2785  rexcom4  2786  ceqsralt  2790  gencbvex  2810  gencbval  2812  ceqsrexbv  2895  euind  2951  reuind  2969  sbccomlem  3064  sbccom  3065  raaan  3556  elxp2  4681  eqbrriv  4758  dm0rn0  4883  dfres2  4998  qfto  5059  xpm  5091  rninxp  5113  fununi  5326  dfoprab2  5969  dfer2  6593  euen1  6861  xpsnen  6880  xpassen  6889  enq0enq  7498  prnmaxl  7555  prnminu  7556  suplocexprlemell  7780