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  2354  2eu8  2654  sbccow  3764  sbcco  3767  dfiin2g  4981  zfpair  5359  dfpo2  6243  dffun6f  6496  fnssintima  7296  imaeqsexvOLD  7297  fsplit  8047  axdc3lem4  10341  addsuniflem  27942  addsasslem1  27944  addsasslem2  27945  addsdilem1  28088  addsdilem2  28089  mulsasslem1  28100  mulsasslem2  28101  renegscl  28398  istrkg2ld  28436  legso  28575  disjunsn  32569  gtiso  32677  fpwrelmapffslem  32710  qqhre  34028  satfdm  35401  dfdm5  35805  dfrn5  35806  brimg  35970  dfrecs2  35983  poimirlem25  37684  cdlemefrs29bpre0  40434  cdlemftr3  40603  dffrege115  44010  brco3f1o  44065  2reu8  47142  ichbi12i  47490  iuneq0  48849  i0oii  48950  setc1onsubc  49633