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 ⊢ (𝜃 ↔ 𝜒)

This proof depends on syntax axioms:   ↔ wb 209

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210

This theorem is used by:  bigolden  1044  sb8f  2383  2eu8  2683  sbccow  3761  sbcco  3764  dfiin2g  4988  zfpair  5382  dfpo2  6299  dffun6f  6553  fnssintima  7372  fsplit  8130  axdc3lem4  10534  addsuniflem  28392  addsasslem1  28394  addsasslem2  28395  addsdilem1  28542  addsdilem2  28543  mulsasslem1  28554  mulsasslem2  28555  elreno2  28886  renegscl  28889  istrkg2ld  28927  legso  29067  disjunsn  33235  gtiso  33341  fpwrelmapffslem  33370  qqhre  34698  satfdm  36220  dfdm5  36629  dfrn5  36630  brimg  36791  dfrecs2  36806  poimirlem25  38656  cdlemefrs29bpre0  41546  cdlemftr3  41715  dffrege115  45071  brco3f1o  45126  2reu8  48275  ichbi12i  48635  iuneq0  50023  i0oii  50127  setc1onsubc  50833