Theorem 3bitr3ri 301

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  1023  2eu8  2660  2ralorOLD  3295  sbccow  3734  sbcco  3737  dfiin2g  4958  zfpair  5339  dfpo2  6188  dffun6f  6432  fsplit  7928  fsplitOLD  7929  axdc3lem4  10140  istrkg2ld  26725  legso  26864  disjunsn  30834  gtiso  30935  fpwrelmapffslem  30969  qqhre  31870  satfdm  33231  fnssintima  33578  imaeqsexv  33593  dfdm5  33653  dfrn5  33654  brimg  34166  dfrecs2  34179  poimirlem25  35729  cdlemefrs29bpre0  38337  cdlemftr3  38506  dffrege115  41475  brco3f1o  41532  elnev  41945  2reu8  44491  ichbi12i  44800  i0oii  46101