Theorem 3bitr3ri 303

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

Syntax hints:   ↔ wb 207

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 208

This theorem is referenced by:  bigolden  1034  sb8f  2362  2eu8  2663  sbccow  3753  sbcco  3756  dfiin2g  4967  zfpair  5357  dfpo2  6254  dffun6f  6507  fnssintima  7313  imaeqsexvOLD  7314  fsplit  8063  axdc3lem4  10373  addsuniflem  28018  addsasslem1  28020  addsasslem2  28021  addsdilem1  28168  addsdilem2  28169  mulsasslem1  28180  mulsasslem2  28181  elreno2  28512  renegscl  28515  istrkg2ld  28553  legso  28692  disjunsn  32690  gtiso  32800  fpwrelmapffslem  32831  qqhre  34211  satfdm  35604  dfdm5  36008  dfrn5  36009  brimg  36170  dfrecs2  36185  poimirlem25  38019  cdlemefrs29bpre0  40895  cdlemftr3  41064  dffrege115  44429  brco3f1o  44484  2reu8  47582  ichbi12i  47942  iuneq0  49316  i0oii  49417  setc1onsubc  50099