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  2384  2eu8  2684  sbccow  3762  sbcco  3765  dfiin2g  4989  zfpair  5383  dfpo2  6292  dffun6f  6546  fnssintima  7364  fsplit  8117  axdc3lem4  10512  addsuniflem  28369  addsasslem1  28371  addsasslem2  28372  addsdilem1  28519  addsdilem2  28520  mulsasslem1  28531  mulsasslem2  28532  elreno2  28863  renegscl  28866  istrkg2ld  28904  legso  29044  disjunsn  33170  gtiso  33276  fpwrelmapffslem  33306  qqhre  34634  satfdm  36103  dfdm5  36507  dfrn5  36508  brimg  36669  dfrecs2  36684  poimirlem25  38531  cdlemefrs29bpre0  41421  cdlemftr3  41590  dffrege115  44937  brco3f1o  44992  2reu8  48126  ichbi12i  48486  iuneq0  49873  i0oii  49972  setc1onsubc  50654