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  558  sbanv  1882  sbexyz  1996  exists1  2115  euxfrdc  2916  euind  2917  rmo4  2923  rmo3f  2927  rmo3  3046  ddifstab  3259  opm  4217  uniuni  4434  rabxp  4646  eliunxp  4748  dmmrnm  4828  imadisj  4971  intirr  4995  resco  5113  funcnv3  5258  fncnv  5262  fun11  5263  fununi  5264  f1mpt  5748  mpomptx  5942  ixp0x  6702  mapsnen  6787  xpcomco  6802  enq0tr  7389  elq  9574  pythagtrip  12230  ntreq0  12891  tx1cn  13028