Theorem 3bitr3ri 289

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

Syntax hints:   ↔ wb 194

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 195

This theorem is referenced by:  bigolden  971  2eu8  2547  2ralor  3087  sbcco  3424  symdifass  3814  dfiin2g  4483  zfpair  4826  dffun6f  5804  fsplit  7146  axdc3lem4  9135  istrkg2ld  25076  legso  25212  disjunsn  28595  gtiso  28667  fpwrelmapffslem  28701  qqhre  29198  dfpo2  30704  dfdm5  30727  dfrn5  30728  nofulllem5  30911  brimg  31020  dfrecs2  31033  poimirlem25  32400  cdlemefrs29bpre0  34498  cdlemftr3  34667  dffrege115  37088  brco3f1o  37147  elnev  37457  2reu8  39638