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

Syntax hints:   ↔ wb 205

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 206

This theorem is referenced by:  bigolden  1024  sb8f  2351  2eu8  2660  2ralorOLD  3297  sbccow  3739  sbcco  3742  dfiin2g  4962  zfpair  5344  dfpo2  6199  dffun6f  6448  fsplit  7957  fsplitOLD  7958  axdc3lem4  10209  istrkg2ld  26821  legso  26960  disjunsn  30933  gtiso  31033  fpwrelmapffslem  31067  qqhre  31970  satfdm  33331  fnssintima  33676  imaeqsexv  33690  dfdm5  33747  dfrn5  33748  brimg  34239  dfrecs2  34252  poimirlem25  35802  cdlemefrs29bpre0  38410  cdlemftr3  38579  dffrege115  41586  brco3f1o  41643  elnev  42056  2reu8  44604  ichbi12i  44912  i0oii  46213