Theorem xchnxbir 323

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 214	. 2 |- ( ph <-> ch )
4	1, 3	xchnxbi 322	1 |- ( -. ch <-> ps )

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

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 197

This theorem is referenced by:  3ioran  1056  hadnot  1541  cadnot  1554  nsspssun  3857  undif3  3888  undif3OLD  3889  intirr  5514  ordtri3or  5755  frxp  7287  ressuppssdif  7316  domunfican  8233  ssfin4  9132  prinfzo0  12506  lcmfunsnlem2lem1  15351  ncoprmlnprm  15436  prm23ge5  15520  symgfix2  17836  gsumdixp  18609  cnfldfunALT  19759  symgmatr01lem  20459  ppttop  20811  zclmncvs  22948  mdegleb  23824  2lgslem3  25129  trlsegvdeg  27087  strlem1  29109  isarchi  29736  bnj1189  31077  dfon3  31999  poimirlem18  33427  poimirlem21  33430  poimirlem30  33439  poimirlem31  33440  ftc1anclem3  33487  hdmaplem4  37063  mapdh9a  37079  ifpnot23  37823  ifpdfxor  37832  ifpnim1  37842  ifpnim2  37844  relintabex  37887  ntrneineine1lem  38382  2exanali  38587  oddneven  41557