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  530  sbanv  1817  sbexyz  1927  exists1  2044  euxfrdc  2801  euind  2802  rmo4  2808  rmo3f  2812  rmo3  2930  ddifstab  3132  opm  4061  uniuni  4273  rabxp  4474  eliunxp  4575  dmmrnm  4655  imadisj  4794  intirr  4818  resco  4935  funcnv3  5076  fncnv  5080  fun11  5081  fununi  5082  f1mpt  5550  mpt2mptx  5739  mapsnen  6528  xpcomco  6542  enq0tr  6993  elq  9107