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  569  sbanv  1944  sbexyz  2063  exists1  2183  euxfrdc  3012  euind  3013  rmo4  3019  rmo3f  3023  rmo3  3144  ddifstab  3361  opm  4372  uniuni  4595  rabxp  4810  eliunxp  4917  dmmrnm  4999  imadisj  5147  intirr  5172  resco  5290  funcnv3  5441  fncnv  5445  fun11  5446  fununi  5447  f1mpt  5971  mpomptx  6173  ixp0x  7002  mapsnen  7094  xpcomco  7118  enq0tr  7795  elq  10005  bitsmod  12706  pythagtrip  13045  ntreq0  15216  tx1cn  15353