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  563  sbanv  1936  sbexyz  2054  exists1  2174  euxfrdc  2989  euind  2990  rmo4  2996  rmo3f  3000  rmo3  3121  ddifstab  3336  opm  4321  uniuni  4543  rabxp  4758  eliunxp  4864  dmmrnm  4946  imadisj  5093  intirr  5118  resco  5236  funcnv3  5386  fncnv  5390  fun11  5391  fununi  5392  f1mpt  5904  mpomptx  6104  ixp0x  6886  mapsnen  6977  xpcomco  6998  enq0tr  7637  elq  9834  bitsmod  12488  pythagtrip  12827  ntreq0  14827  tx1cn  14964