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  1940  sbexyz  2059  exists1  2179  euxfrdc  3006  euind  3007  rmo4  3013  rmo3f  3017  rmo3  3138  ddifstab  3355  opm  4355  uniuni  4577  rabxp  4792  eliunxp  4899  dmmrnm  4981  imadisj  5129  intirr  5154  resco  5272  funcnv3  5423  fncnv  5427  fun11  5428  fununi  5429  f1mpt  5950  mpomptx  6152  ixp0x  6974  mapsnen  7066  xpcomco  7090  enq0tr  7765  elq  9972  bitsmod  12667  pythagtrip  13006  ntreq0  15109  tx1cn  15246