Theorem xchnxbir 307

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 306	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  989  nnelOLD  2800  nsspssun  3728  undif3  3756  ordtri3or  4899  intirr  5373  frxp  6883  ressuppssdif  6913  domunfican  7785  ssfin4  8681  symgfix2  16640  gsumdixpOLD  17452  gsumdixp  17453  symgmatr01lem  19322  ppttop  19675  mdegleb  22630  strlem1  27367  isarchi  27960  dfon3  29770  dvtanlem  30304  ftc1anclem3  30332  2exanali  31534  oddneven  32558  bnj1189  34466  hdmaplem4  37898  mapdh9a  37914  ifpnot23  38119  ifpnim1  38123  ifpnim2  38124  ifpdfxor  38146