Theorem 3bitr2i 208

Description: A chained inference from transitive law for logical equivalence. (Contributed by NM, 4-Aug-2006.)

Hypotheses

Ref	Expression
3bitr2i.1	⊢ (𝜑 ↔ 𝜓)
3bitr2i.2	⊢ (𝜒 ↔ 𝜓)
3bitr2i.3	⊢ (𝜒 ↔ 𝜃)

Assertion

Ref	Expression
3bitr2i	⊢ (𝜑 ↔ 𝜃)

Proof of Theorem 3bitr2i

Step	Hyp	Ref	Expression
1		3bitr2i.1	. . 3 ⊢ (𝜑 ↔ 𝜓)
2		3bitr2i.2	. . 3 ⊢ (𝜒 ↔ 𝜓)
3	1, 2	bitr4i 187	. 2 ⊢ (𝜑 ↔ 𝜒)
4		3bitr2i.3	. 2 ⊢ (𝜒 ↔ 𝜃)
5	3, 4	bitri 184	1 ⊢ (𝜑 ↔ 𝜃)

Syntax hints:   ↔ wb 105

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  an13  563  sbanv  1889  sbexyz  2003  exists1  2122  euxfrdc  2924  euind  2925  rmo4  2931  rmo3f  2935  rmo3  3055  ddifstab  3268  opm  4235  uniuni  4452  rabxp  4664  eliunxp  4767  dmmrnm  4847  imadisj  4991  intirr  5016  resco  5134  funcnv3  5279  fncnv  5283  fun11  5284  fununi  5285  f1mpt  5772  mpomptx  5966  ixp0x  6726  mapsnen  6811  xpcomco  6826  enq0tr  7433  elq  9622  pythagtrip  12283  ntreq0  13635  tx1cn  13772