Theorem 3bitr3ri 305

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

Syntax hints:   ↔ wb 209

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 210

This theorem is referenced by:  bigolden  1042  sb8f  2388  2eu8  2688  sbccow  3770  sbcco  3773  dfiin2g  4991  zfpair  5383  dfpo2  6287  dffun6f  6540  fnssintima  7350  imaeqsexvOLD  7351  fsplit  8100  axdc3lem4  10425  addsuniflem  28152  addsasslem1  28154  addsasslem2  28155  addsdilem1  28302  addsdilem2  28303  mulsasslem1  28314  mulsasslem2  28315  elreno2  28646  renegscl  28649  istrkg2ld  28687  legso  28826  disjunsn  32849  gtiso  32958  fpwrelmapffslem  32989  qqhre  34327  satfdm  35732  dfdm5  36136  dfrn5  36137  brimg  36298  dfrecs2  36313  poimirlem25  38156  cdlemefrs29bpre0  41032  cdlemftr3  41201  dffrege115  44566  brco3f1o  44621  2reu8  47704  ichbi12i  48064  iuneq0  49448  i0oii  49549  setc1onsubc  50231