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  1914  sbexyz  2032  exists1  2151  euxfrdc  2963  euind  2964  rmo4  2970  rmo3f  2974  rmo3  3094  ddifstab  3309  opm  4285  uniuni  4505  rabxp  4719  eliunxp  4824  dmmrnm  4905  imadisj  5052  intirr  5077  resco  5195  funcnv3  5344  fncnv  5348  fun11  5349  fununi  5350  f1mpt  5852  mpomptx  6048  ixp0x  6825  mapsnen  6916  xpcomco  6935  enq0tr  7562  elq  9758  bitsmod  12337  pythagtrip  12676  ntreq0  14674  tx1cn  14811