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  28224  addsasslem1  28226  addsasslem2  28227  addsdilem1  28374  addsdilem2  28375  mulsasslem1  28386  mulsasslem2  28387  elreno2  28718  renegscl  28721  istrkg2ld  28759  legso  28898  disjunsn  32969  gtiso  33076  fpwrelmapffslem  33107  qqhre  34434  satfdm  35874  dfdm5  36278  dfrn5  36279  brimg  36440  dfrecs2  36455  poimirlem25  38329  cdlemefrs29bpre0  41203  cdlemftr3  41372  dffrege115  44737  brco3f1o  44792  2reu8  47882  ichbi12i  48242  iuneq0  49630  i0oii  49731  setc1onsubc  50413