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  2354  2eu8  2657  2ralorOLD  3230  sbccow  3814  sbcco  3817  dfiin2g  5037  zfpair  5427  dfpo2  6318  dffun6f  6581  fnssintima  7382  imaeqsexvOLD  7383  fsplit  8141  axdc3lem4  10491  addsuniflem  28049  addsasslem1  28051  addsasslem2  28052  addsdilem1  28192  addsdilem2  28193  mulsasslem1  28204  mulsasslem2  28205  renegscl  28445  istrkg2ld  28483  legso  28622  disjunsn  32614  gtiso  32716  fpwrelmapffslem  32750  qqhre  33983  satfdm  35354  dfdm5  35754  dfrn5  35755  brimg  35919  dfrecs2  35932  poimirlem25  37632  cdlemefrs29bpre0  40379  cdlemftr3  40548  dffrege115  43968  brco3f1o  44023  2reu8  47062  ichbi12i  47385  i0oii  48716