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  1025  sb8f  2349  2eu8  2658  2ralorOLD  3220  sbccow  3762  sbcco  3765  dfiin2g  4992  zfpair  5376  dfpo2  6248  dffun6f  6514  fnssintima  7306  imaeqsexv  7307  fsplit  8048  axdc3lem4  10388  addsunif  27308  addsasslem1  27309  addsasslem2  27310  istrkg2ld  27400  legso  27539  disjunsn  31510  gtiso  31610  fpwrelmapffslem  31644  qqhre  32592  satfdm  33954  dfdm5  34338  dfrn5  34339  brimg  34513  dfrecs2  34526  poimirlem25  36094  cdlemefrs29bpre0  38850  cdlemftr3  39019  dffrege115  42232  brco3f1o  42287  elnev  42700  2reu8  45316  ichbi12i  45624  i0oii  46924