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  1027  sb8f  2359  2eu8  2662  2ralorOLD  3238  sbccow  3827  sbcco  3830  dfiin2g  5055  zfpair  5439  dfpo2  6327  dffun6f  6591  fnssintima  7398  imaeqsexvOLD  7399  fsplit  8158  axdc3lem4  10522  addsuniflem  28052  addsasslem1  28054  addsasslem2  28055  addsdilem1  28195  addsdilem2  28196  mulsasslem1  28207  mulsasslem2  28208  renegscl  28448  istrkg2ld  28486  legso  28625  disjunsn  32616  gtiso  32712  fpwrelmapffslem  32746  qqhre  33966  satfdm  35337  dfdm5  35736  dfrn5  35737  brimg  35901  dfrecs2  35914  poimirlem25  37605  cdlemefrs29bpre0  40353  cdlemftr3  40522  dffrege115  43940  brco3f1o  43995  2reu8  47027  ichbi12i  47334  i0oii  48599