Theorem 3bitr2i 208

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

Syntax hints:   ↔ wb 105

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  an13  565  sbanv  1938  sbexyz  2056  exists1  2176  euxfrdc  2992  euind  2993  rmo4  2999  rmo3f  3003  rmo3  3124  ddifstab  3339  opm  4326  uniuni  4548  rabxp  4763  eliunxp  4869  dmmrnm  4951  imadisj  5098  intirr  5123  resco  5241  funcnv3  5392  fncnv  5396  fun11  5397  fununi  5398  f1mpt  5912  mpomptx  6112  ixp0x  6895  mapsnen  6986  xpcomco  7010  enq0tr  7654  elq  9856  bitsmod  12522  pythagtrip  12861  ntreq0  14862  tx1cn  14999