Theorem 3bitr3ri 304

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 279	. 2 ⊢ (𝜓 ↔ 𝜒)
5	1, 4	bitr3i 279	1 ⊢ (𝜃 ↔ 𝜒)

Syntax hints:   ↔ wb 208

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 209

This theorem is referenced by:  bigolden  1039  sb8f  2384  2eu8  2684  sbccow  3767  sbcco  3770  dfiin2g  4987  zfpair  5377  dfpo2  6279  dffun6f  6532  fnssintima  7342  imaeqsexvOLD  7343  fsplit  8091  axdc3lem4  10407  addsuniflem  28071  addsasslem1  28073  addsasslem2  28074  addsdilem1  28221  addsdilem2  28222  mulsasslem1  28233  mulsasslem2  28234  elreno2  28565  renegscl  28568  istrkg2ld  28606  legso  28745  disjunsn  32743  gtiso  32853  fpwrelmapffslem  32884  qqhre  34278  satfdm  35683  dfdm5  36087  dfrn5  36088  brimg  36249  dfrecs2  36264  poimirlem25  38108  cdlemefrs29bpre0  40984  cdlemftr3  41153  dffrege115  44518  brco3f1o  44573  2reu8  47670  ichbi12i  48030  iuneq0  49404  i0oii  49505  setc1onsubc  50187