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  1029  sb8f  2358  2eu8  2659  sbccow  3751  sbcco  3754  dfiin2g  4973  zfpair  5363  dfpo2  6260  dffun6f  6513  fnssintima  7317  imaeqsexvOLD  7318  fsplit  8067  axdc3lem4  10375  addsuniflem  27993  addsasslem1  27995  addsasslem2  27996  addsdilem1  28143  addsdilem2  28144  mulsasslem1  28155  mulsasslem2  28156  elreno2  28487  renegscl  28490  istrkg2ld  28528  legso  28667  disjunsn  32664  gtiso  32774  fpwrelmapffslem  32805  qqhre  34164  satfdm  35551  dfdm5  35955  dfrn5  35956  brimg  36117  dfrecs2  36132  poimirlem25  37966  cdlemefrs29bpre0  40842  cdlemftr3  41011  dffrege115  44405  brco3f1o  44460  2reu8  47560  ichbi12i  47920  iuneq0  49294  i0oii  49395  setc1onsubc  50077