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  1901  sbexyz  2015  exists1  2134  euxfrdc  2938  euind  2939  rmo4  2945  rmo3f  2949  rmo3  3069  ddifstab  3282  opm  4249  uniuni  4466  rabxp  4678  eliunxp  4781  dmmrnm  4861  imadisj  5005  intirr  5030  resco  5148  funcnv3  5293  fncnv  5297  fun11  5298  fununi  5299  f1mpt  5788  mpomptx  5982  ixp0x  6744  mapsnen  6829  xpcomco  6844  enq0tr  7451  elq  9640  pythagtrip  12301  ntreq0  14029  tx1cn  14166