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  1028  sb8f  2358  2eu8  2659  sbccow  3763  sbcco  3766  dfiin2g  4986  zfpair  5366  dfpo2  6254  dffun6f  6507  fnssintima  7308  imaeqsexvOLD  7309  fsplit  8059  axdc3lem4  10363  addsuniflem  27997  addsasslem1  27999  addsasslem2  28000  addsdilem1  28147  addsdilem2  28148  mulsasslem1  28159  mulsasslem2  28160  elreno2  28491  renegscl  28494  istrkg2ld  28532  legso  28671  disjunsn  32669  gtiso  32780  fpwrelmapffslem  32811  qqhre  34177  satfdm  35563  dfdm5  35967  dfrn5  35968  brimg  36129  dfrecs2  36144  poimirlem25  37846  cdlemefrs29bpre0  40656  cdlemftr3  40825  dffrege115  44219  brco3f1o  44274  2reu8  47358  ichbi12i  47706  iuneq0  49064  i0oii  49165  setc1onsubc  49847