Theorem xchnxbir 310

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

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

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 188

This theorem is referenced by:  3ioran  1000  hadnot  1500  cadnot  1513  nnelOLD  2771  nsspssun  3706  undif3  3734  intirr  5234  ordtri3or  5471  frxp  6914  ressuppssdif  6944  domunfican  7847  ssfin4  8741  lcmfunsnlem2lem1  14599  ncoprmlnprm  14665  symgfix2  17045  gsumdixp  17825  symgmatr01lem  19665  ppttop  20009  mdegleb  23000  strlem1  27889  isarchi  28494  bnj1189  29814  dfon3  30652  poimirlem18  31872  poimirlem21  31875  poimirlem30  31884  poimirlem31  31885  dvtanlemOLD  31905  ftc1anclem3  31933  hdmaplem4  35261  mapdh9a  35277  ifpnot23  36042  ifpdfxor  36051  ifpnim1  36061  ifpnim2  36063  2exanali  36595  oddneven  38486