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 ⊢ (𝜃 ↔ 𝜒)

This proof depends on syntax axioms:   ↔ wb 209

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210

This theorem is used by:  bigolden  1044  sb8f  2389  2eu8  2689  sbccow  3770  sbcco  3773  dfiin2g  5000  zfpair  5397  dfpo2  6304  dffun6f  6558  fnssintima  7373  imaeqsexvOLD  7374  fsplit  8121  axdc3lem4  10455  addsuniflem  28231  addsasslem1  28233  addsasslem2  28234  addsdilem1  28381  addsdilem2  28382  mulsasslem1  28393  mulsasslem2  28394  elreno2  28725  renegscl  28728  istrkg2ld  28766  legso  28905  disjunsn  32976  gtiso  33083  fpwrelmapffslem  33114  qqhre  34441  satfdm  35882  dfdm5  36286  dfrn5  36287  brimg  36448  dfrecs2  36463  poimirlem25  38337  cdlemefrs29bpre0  41211  cdlemftr3  41380  dffrege115  44745  brco3f1o  44800  2reu8  47890  ichbi12i  48250  iuneq0  49638  i0oii  49739  setc1onsubc  50421