Theorem 3bitr3ri 302

Description: A chained inference from transitive law for logical equivalence. (Contributed by NM, 21-Jun-1993.)

Hypotheses

Ref	Expression
3bitr3i.1	⊢ (𝜑 ↔ 𝜓)
3bitr3i.2	⊢ (𝜑 ↔ 𝜒)
3bitr3i.3	⊢ (𝜓 ↔ 𝜃)

Assertion

Ref	Expression
3bitr3ri	⊢ (𝜃 ↔ 𝜒)

Proof of Theorem 3bitr3ri

Step	Hyp	Ref	Expression
1		3bitr3i.3	. 2 ⊢ (𝜓 ↔ 𝜃)
2		3bitr3i.1	. . 3 ⊢ (𝜑 ↔ 𝜓)
3		3bitr3i.2	. . 3 ⊢ (𝜑 ↔ 𝜒)
4	2, 3	bitr3i 277	. 2 ⊢ (𝜓 ↔ 𝜒)
5	1, 4	bitr3i 277	1 ⊢ (𝜃 ↔ 𝜒)

Syntax hints:   ↔ wb 206

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 207

This theorem is referenced by:  bigolden  1029  sb8f  2359  2eu8  2660  sbccow  3765  sbcco  3768  dfiin2g  4988  zfpair  5368  dfpo2  6262  dffun6f  6515  fnssintima  7318  imaeqsexvOLD  7319  fsplit  8069  axdc3lem4  10375  addsuniflem  28009  addsasslem1  28011  addsasslem2  28012  addsdilem1  28159  addsdilem2  28160  mulsasslem1  28171  mulsasslem2  28172  elreno2  28503  renegscl  28506  istrkg2ld  28544  legso  28683  disjunsn  32680  gtiso  32790  fpwrelmapffslem  32821  qqhre  34197  satfdm  35582  dfdm5  35986  dfrn5  35987  brimg  36148  dfrecs2  36163  poimirlem25  37890  cdlemefrs29bpre0  40766  cdlemftr3  40935  dffrege115  44328  brco3f1o  44383  2reu8  47466  ichbi12i  47814  iuneq0  49172  i0oii  49273  setc1onsubc  49955