Theorem 3bitr2i 208

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 187	. 2 |- ( ph <-> ch )
4		3bitr2i.3	. 2 |- ( ch <-> th )
5	3, 4	bitri 184	1 |- ( ph <-> th )

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  2152  euxfrdc  2966  euind  2967  rmo4  2973  rmo3f  2977  rmo3  3098  ddifstab  3313  opm  4296  uniuni  4516  rabxp  4730  eliunxp  4835  dmmrnm  4916  imadisj  5063  intirr  5088  resco  5206  funcnv3  5355  fncnv  5359  fun11  5360  fununi  5361  f1mpt  5863  mpomptx  6059  ixp0x  6836  mapsnen  6927  xpcomco  6946  enq0tr  7582  elq  9778  bitsmod  12382  pythagtrip  12721  ntreq0  14719  tx1cn  14856