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

Syntax hints:   ↔ wb 206

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 207

This theorem is referenced by:  bigolden  1028  sb8f  2352  2eu8  2652  sbccow  3767  sbcco  3770  dfiin2g  4984  zfpair  5363  dfpo2  6248  dffun6f  6501  fnssintima  7303  imaeqsexvOLD  7304  fsplit  8057  axdc3lem4  10366  addsuniflem  27931  addsasslem1  27933  addsasslem2  27934  addsdilem1  28077  addsdilem2  28078  mulsasslem1  28089  mulsasslem2  28090  renegscl  28385  istrkg2ld  28423  legso  28562  disjunsn  32556  gtiso  32657  fpwrelmapffslem  32688  qqhre  33986  satfdm  35341  dfdm5  35745  dfrn5  35746  brimg  35910  dfrecs2  35923  poimirlem25  37624  cdlemefrs29bpre0  40375  cdlemftr3  40544  dffrege115  43951  brco3f1o  44006  2reu8  47097  ichbi12i  47445  iuneq0  48804  i0oii  48905  setc1onsubc  49588