Theorem 3bitr3ri 301

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

Syntax hints:   ↔ wb 205

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 206

This theorem is referenced by:  bigolden  1023  sb8f  2347  2eu8  2652  2ralorOLD  3227  sbccow  3799  sbcco  3802  dfiin2g  5034  zfpair  5418  dfpo2  6294  dffun6f  6560  fnssintima  7361  imaeqsexv  7362  fsplit  8105  axdc3lem4  10450  addsuniflem  27723  addsasslem1  27725  addsasslem2  27726  addsdilem1  27845  addsdilem2  27846  mulsasslem1  27857  mulsasslem2  27858  istrkg2ld  27978  legso  28117  disjunsn  32092  gtiso  32189  fpwrelmapffslem  32224  qqhre  33298  satfdm  34658  dfdm5  35048  dfrn5  35049  brimg  35213  dfrecs2  35226  poimirlem25  36816  cdlemefrs29bpre0  39570  cdlemftr3  39739  dffrege115  43031  brco3f1o  43086  2reu8  46118  ichbi12i  46426  i0oii  47639