Theorem 3bitr2i 207

Description: A chained inference from transitive law for logical equivalence. (Contributed by NM, 4-Aug-2006.)

Hypotheses

Ref	Expression
3bitr2i.1	|- ( ph <-> ps )
3bitr2i.2	|- ( ch <-> ps )
3bitr2i.3	|- ( ch <-> th )

Assertion

Ref	Expression
3bitr2i	|- ( ph <-> th )

Proof of Theorem 3bitr2i

Step	Hyp	Ref	Expression
1		3bitr2i.1	. . 3 |- ( ph <-> ps )
2		3bitr2i.2	. . 3 |- ( ch <-> ps )
3	1, 2	bitr4i 186	. 2 |- ( ph <-> ch )
4		3bitr2i.3	. 2 |- ( ch <-> th )
5	3, 4	bitri 183	1 |- ( ph <-> th )

Syntax hints:   <-> wb 104

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  an13  558  sbanv  1882  sbexyz  1996  exists1  2115  euxfrdc  2916  euind  2917  rmo4  2923  rmo3f  2927  rmo3  3046  ddifstab  3259  opm  4219  uniuni  4436  rabxp  4648  eliunxp  4750  dmmrnm  4830  imadisj  4973  intirr  4997  resco  5115  funcnv3  5260  fncnv  5264  fun11  5265  fununi  5266  f1mpt  5750  mpomptx  5944  ixp0x  6704  mapsnen  6789  xpcomco  6804  enq0tr  7396  elq  9581  pythagtrip  12237  ntreq0  12926  tx1cn  13063