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  3752  sbcco  3755  dfiin2g  4974  zfpair  5358  dfpo2  6254  dffun6f  6507  fnssintima  7310  imaeqsexvOLD  7311  fsplit  8060  axdc3lem4  10366  addsuniflem  28007  addsasslem1  28009  addsasslem2  28010  addsdilem1  28157  addsdilem2  28158  mulsasslem1  28169  mulsasslem2  28170  elreno2  28501  renegscl  28504  istrkg2ld  28542  legso  28681  disjunsn  32679  gtiso  32789  fpwrelmapffslem  32820  qqhre  34180  satfdm  35567  dfdm5  35971  dfrn5  35972  brimg  36133  dfrecs2  36148  poimirlem25  37980  cdlemefrs29bpre0  40856  cdlemftr3  41025  dffrege115  44423  brco3f1o  44478  2reu8  47572  ichbi12i  47932  iuneq0  49306  i0oii  49407  setc1onsubc  50089