Theorem 3bitr2i 207

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

Syntax hints:   ↔ wb 104

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

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  an13  553  sbanv  1877  sbexyz  1991  exists1  2110  euxfrdc  2911  euind  2912  rmo4  2918  rmo3f  2922  rmo3  3041  ddifstab  3253  opm  4211  uniuni  4428  rabxp  4640  eliunxp  4742  dmmrnm  4822  imadisj  4965  intirr  4989  resco  5107  funcnv3  5249  fncnv  5253  fun11  5254  fununi  5255  f1mpt  5738  mpomptx  5929  ixp0x  6688  mapsnen  6773  xpcomco  6788  enq0tr  7371  elq  9556  pythagtrip  12211  ntreq0  12732  tx1cn  12869