Theorem 3bitr2i 197

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

Syntax hints:   ↔ wb 98

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101

This theorem depends on definitions:  df-bi 110

This theorem is referenced by:  an13  497  sbanv  1769  sbexyz  1879  exists1  1996  euxfrdc  2727  euind  2728  rmo4  2734  rmo3  2849  opm  3971  uniuni  4183  rabxp  4380  eliunxp  4475  dmmrnm  4554  imadisj  4687  intirr  4711  resco  4825  funcnv3  4961  fncnv  4965  fun11  4966  fununi  4967  f1mpt  5410  mpt2mptx  5595  xpcomco  6300  enq0tr  6532  elq  8557