Theorem 3bitr2i 206

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

Syntax hints:   ↔ wb 103

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

This theorem depends on definitions:  df-bi 115

This theorem is referenced by:  an13  528  sbanv  1812  sbexyz  1922  exists1  2039  euxfrdc  2789  euind  2790  rmo4  2796  rmo3  2916  ddifstab  3116  opm  4025  uniuni  4237  rabxp  4436  eliunxp  4533  dmmrnm  4613  imadisj  4749  intirr  4773  resco  4889  funcnv3  5029  fncnv  5033  fun11  5034  fununi  5035  f1mpt  5490  mpt2mptx  5674  mapsnen  6458  xpcomco  6472  enq0tr  6896  elq  9002