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 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  1026  sb8f  2350  2eu8  2655  2ralorOLD  3230  sbccow  3801  sbcco  3804  dfiin2g  5036  zfpair  5420  dfpo2  6296  dffun6f  6562  fnssintima  7359  imaeqsexv  7360  fsplit  8103  axdc3lem4  10448  addsuniflem  27484  addsasslem1  27486  addsasslem2  27487  addsdilem1  27606  addsdilem2  27607  mulsasslem1  27618  mulsasslem2  27619  istrkg2ld  27711  legso  27850  disjunsn  31825  gtiso  31922  fpwrelmapffslem  31957  qqhre  33000  satfdm  34360  dfdm5  34744  dfrn5  34745  brimg  34909  dfrecs2  34922  poimirlem25  36513  cdlemefrs29bpre0  39267  cdlemftr3  39436  dffrege115  42729  brco3f1o  42784  2reu8  45820  ichbi12i  46128  i0oii  47552