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  2356  2eu8  2659  2ralorOLD  3220  sbccow  3793  sbcco  3796  dfiin2g  5013  zfpair  5396  dfpo2  6290  dffun6f  6554  fnssintima  7360  imaeqsexvOLD  7361  fsplit  8121  axdc3lem4  10472  addsuniflem  27965  addsasslem1  27967  addsasslem2  27968  addsdilem1  28111  addsdilem2  28112  mulsasslem1  28123  mulsasslem2  28124  renegscl  28406  istrkg2ld  28444  legso  28583  disjunsn  32580  gtiso  32683  fpwrelmapffslem  32714  qqhre  34056  satfdm  35396  dfdm5  35795  dfrn5  35796  brimg  35960  dfrecs2  35973  poimirlem25  37674  cdlemefrs29bpre0  40420  cdlemftr3  40589  dffrege115  43969  brco3f1o  44024  2reu8  47108  ichbi12i  47441  iuneq0  48764  i0oii  48861  setc1onsubc  49446