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-1 5  ax-2 6  ax-3 7  ax-mp 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  3022  rmo4  3029  2reu5lem3  3043  rmo3  3133  difin  3492  difin0ss  3616  elp6  4263  eqtfinrelk  4486  nnpweqlem1  4522  setconslem1  4731  setconslem6  4736  rabxp  4814  eliunxp  4821  dmeq0  4922  imadisj  5015  eliniseg  5020  intirr  5029  resco  5085  funcnv3  5157  fncnv  5158  fun11  5159  fununi  5160  iunfopab  5204  abrexco  5463  fnov  5591  mpt2mptx  5708  brtxp  5783  composeex  5820  addcfnex  5824  brpprod  5839  crossex  5850  domfnex  5870  ranfnex  5871  clos1ex  5876  clos1induct  5880  refex  5911  antisymex  5912  connexex  5913  extex  5915  symex  5916  mapexi  6003  enmap2lem1  6063  lecex  6115  mucex  6133  ceexlem1  6173  nncdiv3lem1  6275  nncdiv3  6277  nchoicelem16  6304  fnfreclem1  6317