Theorem 3bitr2i 207

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 186	. 2 ⊢ (𝜑 ↔ 𝜒)
4		3bitr2i.3	. 2 ⊢ (𝜒 ↔ 𝜃)
5	3, 4	bitri 183	1 ⊢ (𝜑 ↔ 𝜃)

Syntax hints:   ↔ wb 104

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

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  an13  553  sbanv  1862  sbexyz  1979  exists1  2096  euxfrdc  2874  euind  2875  rmo4  2881  rmo3f  2885  rmo3  3004  ddifstab  3213  opm  4164  uniuni  4380  rabxp  4584  eliunxp  4686  dmmrnm  4766  imadisj  4909  intirr  4933  resco  5051  funcnv3  5193  fncnv  5197  fun11  5198  fununi  5199  f1mpt  5680  mpomptx  5870  ixp0x  6628  mapsnen  6713  xpcomco  6728  enq0tr  7266  elq  9441  ntreq0  12340  tx1cn  12477