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  1933  cbvex2  1934  sbco2vh  1957  equsb3  1963  sbn  1964  sbim  1965  sbor  1966  sban  1967  sbco2h  1976  sbco2d  1978  sbco2vd  1979  sbcomv  1983  sbco3  1986  sbcom  1987  sbcom2v  1997  sbcom2v2  1998  sbcom2  1999  dfsb7  2003  sb7f  2004  sb7af  2005  sbal  2012  sbex  2016  sbco4lem  2018  moanim  2112  eq2tri  2249  eqsb1  2293  clelsb1  2294  clelsb2  2295  clelsb1f  2336  ralcom4  2774  rexcom4  2775  ceqsralt  2779  gencbvex  2798  gencbval  2800  ceqsrexbv  2883  euind  2939  reuind  2957  sbccomlem  3052  sbccom  3053  raaan  3544  elxp2  4662  eqbrriv  4739  dm0rn0  4862  dfres2  4977  qfto  5036  xpm  5068  rninxp  5090  fununi  5303  dfoprab2  5943  dfer2  6560  euen1  6828  xpsnen  6847  xpassen  6856  enq0enq  7460  prnmaxl  7517  prnminu  7518  suplocexprlemell  7742