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  2656  sbccow  3760  sbcco  3763  dfiin2g  4981  zfpair  5361  dfpo2  6248  dffun6f  6501  fnssintima  7302  imaeqsexvOLD  7303  fsplit  8053  axdc3lem4  10351  addsuniflem  27945  addsasslem1  27947  addsasslem2  27948  addsdilem1  28091  addsdilem2  28092  mulsasslem1  28103  mulsasslem2  28104  renegscl  28401  istrkg2ld  28439  legso  28578  disjunsn  32576  gtiso  32686  fpwrelmapffslem  32719  qqhre  34054  satfdm  35434  dfdm5  35838  dfrn5  35839  brimg  36000  dfrecs2  36015  poimirlem25  37705  cdlemefrs29bpre0  40515  cdlemftr3  40684  dffrege115  44095  brco3f1o  44150  2reu8  47236  ichbi12i  47584  iuneq0  48943  i0oii  49044  setc1onsubc  49727