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  2744  2ralor  3369  sbccow  3795  sbcco  3798  dfiin2g  4957  zfpair  5322  dffun6f  6369  fsplit  7812  fsplitOLD  7813  axdc3lem4  9875  istrkg2ld  26246  legso  26385  disjunsn  30344  gtiso  30436  fpwrelmapffslem  30468  qqhre  31261  satfdm  32616  dfpo2  32991  dfdm5  33016  dfrn5  33017  brimg  33398  dfrecs2  33411  poimirlem25  34932  cdlemefrs29bpre0  37547  cdlemftr3  37716  dffrege115  40344  brco3f1o  40403  elnev  40790  2reu8  43331  ichbi12i  43638