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  2653  sbccow  3779  sbcco  3782  dfiin2g  4999  zfpair  5379  dfpo2  6272  dffun6f  6532  fnssintima  7340  imaeqsexvOLD  7341  fsplit  8099  axdc3lem4  10413  addsuniflem  27915  addsasslem1  27917  addsasslem2  27918  addsdilem1  28061  addsdilem2  28062  mulsasslem1  28073  mulsasslem2  28074  renegscl  28356  istrkg2ld  28394  legso  28533  disjunsn  32530  gtiso  32631  fpwrelmapffslem  32662  qqhre  34017  satfdm  35363  dfdm5  35767  dfrn5  35768  brimg  35932  dfrecs2  35945  poimirlem25  37646  cdlemefrs29bpre0  40397  cdlemftr3  40566  dffrege115  43974  brco3f1o  44029  2reu8  47117  ichbi12i  47465  iuneq0  48811  i0oii  48912  setc1onsubc  49595