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-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  an13  535  sbanv  1843  sbexyz  1954  exists1  2071  euxfrdc  2839  euind  2840  rmo4  2846  rmo3f  2850  rmo3  2968  ddifstab  3174  opm  4116  uniuni  4332  rabxp  4536  eliunxp  4638  dmmrnm  4718  imadisj  4859  intirr  4883  resco  5001  funcnv3  5143  fncnv  5147  fun11  5148  fununi  5149  f1mpt  5626  mpomptx  5816  ixp0x  6574  mapsnen  6659  xpcomco  6673  enq0tr  7190  elq  9316  ntreq0  12144  tx1cn  12280