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  527  sbanv  1810  sbexyz  1920  exists1  2037  euxfrdc  2778  euind  2779  rmo4  2785  rmo3  2905  ddifstab  3104  opm  3989  uniuni  4201  rabxp  4398  eliunxp  4493  dmmrnm  4572  imadisj  4707  intirr  4731  resco  4845  funcnv3  4981  fncnv  4985  fun11  4986  fununi  4987  f1mpt  5431  mpt2mptx  5615  xpcomco  6323  enq0tr  6624  elq  8707