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  1939  sbexyz  2057  exists1  2177  euxfrdc  3002  euind  3003  rmo4  3009  rmo3f  3013  rmo3  3134  ddifstab  3350  opm  4349  uniuni  4571  rabxp  4786  eliunxp  4893  dmmrnm  4975  imadisj  5123  intirr  5148  resco  5266  funcnv3  5417  fncnv  5421  fun11  5422  fununi  5423  f1mpt  5943  mpomptx  6143  ixp0x  6960  mapsnen  7052  xpcomco  7076  enq0tr  7748  elq  9953  bitsmod  12638  pythagtrip  12977  ntreq0  14989  tx1cn  15126