Theorem xchnxbir 309

Description: Replacement of a subexpression by an equivalent one. (Contributed by Wolf Lammen, 27-Sep-2014.)

Hypotheses

Ref	Expression
xchnxbir.1	|- ( -. ph <-> ps )
xchnxbir.2	|- ( ch <-> ph )

Assertion

Ref	Expression
xchnxbir	|- ( -. ch <-> ps )

Proof of Theorem xchnxbir

Step	Hyp	Ref	Expression
1		xchnxbir.1	. 2 |- ( -. ph <-> ps )
2		xchnxbir.2	. . 3 |- ( ch <-> ph )
3	2	bicomi 202	. 2 |- ( ph <-> ch )
4	1, 3	xchnxbi 308	1 |- ( -. ch <-> ps )

Syntax hints:   -. wn 3   <-> wb 184

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 185

This theorem is referenced by:  3ioran  983  nnelOLD  2791  nsspssun  3667  undif3  3695  ordtri3or  4835  intirr  5300  frxp  6768  ressuppssdif  6796  domunfican  7671  ssfin4  8566  wrdsymb0  12347  symgfix2  16009  gsumdixpOLD  16792  gsumdixp  16793  symgmatr01lem  18561  ppttop  18713  mdegleb  21637  strlem1  25775  isarchi  26319  dfon3  28043  dvtanlem  28565  ftc1anclem3  28593  2exanali  29764  bnj1189  32282  hdmaplem4  35701  mapdh9a  35717