Theorem 3bitr3ri 291

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

Syntax hints:   ↔ wb 196

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 197

This theorem is referenced by:  bigolden  1014  2eu8  2698  2ralor  3247  sbcco  3599  symdifass  3996  dfiin2g  4705  zfpair  5053  dffun6f  6063  fsplit  7451  axdc3lem4  9487  istrkg2ld  25579  legso  25714  disjunsn  29735  gtiso  29808  fpwrelmapffslem  29837  qqhre  30394  dfpo2  31973  dfdm5  32002  dfrn5  32003  brimg  32371  dfrecs2  32384  poimirlem25  33765  cdlemefrs29bpre0  36204  cdlemftr3  36373  dffrege115  38792  brco3f1o  38851  elnev  39159  2reu8  41716