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  2993  euind  2994  rmo4  3000  rmo3f  3004  rmo3  3125  ddifstab  3341  opm  4332  uniuni  4554  rabxp  4769  eliunxp  4875  dmmrnm  4957  imadisj  5105  intirr  5130  resco  5248  funcnv3  5399  fncnv  5403  fun11  5404  fununi  5405  f1mpt  5922  mpomptx  6122  ixp0x  6938  mapsnen  7029  xpcomco  7053  enq0tr  7697  elq  9899  bitsmod  12578  pythagtrip  12917  ntreq0  14923  tx1cn  15060