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  37842  cdlemefrs29bpre0  40652  cdlemftr3  40821  dffrege115  44215  brco3f1o  44270  2reu8  47354  ichbi12i  47702  iuneq0  49060  i0oii  49161  setc1onsubc  49843