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  1766  sbexyz  1876  exists1  1993  euxfrdc  2721  euind  2722  rmo4  2728  rmo3  2843  opm  3962  uniuni  4149  rabxp  4323  eliunxp  4418  dmmrnm  4497  imadisj  4630  intirr  4654  resco  4768  funcnv3  4904  fncnv  4908  fun11  4909  fununi  4910  f1mpt  5353  mpt2mptx  5537  xpcomco  6236  enq0tr  6416  elq  8313