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  2352  2eu8  2652  sbccow  3776  sbcco  3779  dfiin2g  4996  zfpair  5376  dfpo2  6269  dffun6f  6529  fnssintima  7337  imaeqsexvOLD  7338  fsplit  8096  axdc3lem4  10406  addsuniflem  27908  addsasslem1  27910  addsasslem2  27911  addsdilem1  28054  addsdilem2  28055  mulsasslem1  28066  mulsasslem2  28067  renegscl  28349  istrkg2ld  28387  legso  28526  disjunsn  32523  gtiso  32624  fpwrelmapffslem  32655  qqhre  34010  satfdm  35356  dfdm5  35760  dfrn5  35761  brimg  35925  dfrecs2  35938  poimirlem25  37639  cdlemefrs29bpre0  40390  cdlemftr3  40559  dffrege115  43967  brco3f1o  44022  2reu8  47113  ichbi12i  47461  iuneq0  48807  i0oii  48908  setc1onsubc  49591