Theorem 3bitr2i 264

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 243	. 2 ⊢ (φ ↔ χ)
4		3bitr2i.3	. 2 ⊢ (χ ↔ θ)
5	3, 4	bitri 240	1 ⊢ (φ ↔ θ)

Syntax hints:   ↔ wb 176

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 177

This theorem is referenced by:  con2bi  318  an13  774  xorneg1  1311  2eu5  2288  exists1  2293  euxfr  3023  rmo4  3030  2reu5lem3  3044  rmo3  3134  difin  3493  difin0ss  3617  elp6  4264  eqtfinrelk  4487  nnpweqlem1  4523  setconslem1  4732  setconslem6  4737  rabxp  4815  eliunxp  4822  dmeq0  4923  imadisj  5016  eliniseg  5021  intirr  5030  resco  5086  funcnv3  5158  fncnv  5159  fun11  5160  fununi  5161  iunfopab  5205  abrexco  5464  fnov  5592  mpt2mptx  5709  brtxp  5784  composeex  5821  addcfnex  5825  brpprod  5840  crossex  5851  domfnex  5871  ranfnex  5872  clos1ex  5877  clos1induct  5881  refex  5912  antisymex  5913  connexex  5914  extex  5916  symex  5917  mapexi  6004  enmap2lem1  6064  lecex  6116  mucex  6134  ceexlem1  6174  nncdiv3lem1  6276  nncdiv3  6278  nchoicelem16  6305  fnfreclem1  6318