Theorem 3bitr3ri 305

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

Syntax hints:   ↔ wb 209

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 210

This theorem is referenced by:  bigolden  1044  sb8f  2386  2eu8  2686  sbccow  3768  sbcco  3771  dfiin2g  4996  zfpair  5394  dfpo2  6299  dffun6f  6553  fnssintima  7362  imaeqsexvOLD  7363  fsplit  8113  axdc3lem4  10438  addsuniflem  28172  addsasslem1  28174  addsasslem2  28175  addsdilem1  28322  addsdilem2  28323  mulsasslem1  28334  mulsasslem2  28335  elreno2  28666  renegscl  28669  istrkg2ld  28707  legso  28846  disjunsn  32917  gtiso  33024  fpwrelmapffslem  33055  qqhre  34388  satfdm  35839  dfdm5  36243  dfrn5  36244  brimg  36405  dfrecs2  36420  poimirlem25  38274  cdlemefrs29bpre0  41148  cdlemftr3  41317  dffrege115  44684  brco3f1o  44739  2reu8  47826  ichbi12i  48186  iuneq0  49574  i0oii  49675  setc1onsubc  50357