Theorem 3bitr3ri 304

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

Syntax hints:   ↔ wb 208

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 209

This theorem is referenced by:  bigolden  1023  2eu8  2742  2ralor  3370  sbccow  3795  sbcco  3798  dfiin2g  4950  zfpair  5314  dffun6f  6364  fsplit  7806  fsplitOLD  7807  axdc3lem4  9869  istrkg2ld  26240  legso  26379  disjunsn  30338  gtiso  30430  fpwrelmapffslem  30462  qqhre  31256  satfdm  32611  dfpo2  32986  dfdm5  33011  dfrn5  33012  brimg  33393  dfrecs2  33406  poimirlem25  34911  cdlemefrs29bpre0  37526  cdlemftr3  37695  dffrege115  40317  brco3f1o  40376  elnev  40763  2reu8  43304  ichbi12i  43611