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  1919  cbvex2  1920  sbco2vh  1943  equsb3  1949  sbn  1950  sbim  1951  sbor  1952  sban  1953  sbco2h  1962  sbco2d  1964  sbco2vd  1965  sbcomv  1969  sbco3  1972  sbcom  1973  sbcom2v  1983  sbcom2v2  1984  sbcom2  1985  dfsb7  1989  sb7f  1990  sb7af  1991  sbal  1998  sbex  2002  sbco4lem  2004  moanim  2098  eq2tri  2235  eqsb1  2279  clelsb1  2280  clelsb2  2281  clelsb1f  2321  ralcom4  2757  rexcom4  2758  ceqsralt  2762  gencbvex  2781  gencbval  2783  ceqsrexbv  2866  euind  2922  reuind  2940  sbccomlem  3035  sbccom  3036  raaan  3527  elxp2  4638  eqbrriv  4715  dm0rn0  4837  dfres2  4952  qfto  5010  xpm  5042  rninxp  5064  fununi  5276  dfoprab2  5912  dfer2  6526  euen1  6792  xpsnen  6811  xpassen  6820  enq0enq  7405  prnmaxl  7462  prnminu  7463  suplocexprlemell  7687