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  553  sbanv  1877  sbexyz  1991  exists1  2110  euxfrdc  2912  euind  2913  rmo4  2919  rmo3f  2923  rmo3  3042  ddifstab  3254  opm  4212  uniuni  4429  rabxp  4641  eliunxp  4743  dmmrnm  4823  imadisj  4966  intirr  4990  resco  5108  funcnv3  5250  fncnv  5254  fun11  5255  fununi  5256  f1mpt  5739  mpomptx  5933  ixp0x  6692  mapsnen  6777  xpcomco  6792  enq0tr  7375  elq  9560  pythagtrip  12215  ntreq0  12772  tx1cn  12909