Theorem xchnxbir 309

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

Hypotheses

Ref	Expression
xchnxbir.1
xchnxbir.2

Assertion

Ref	Expression
xchnxbir

Proof of Theorem xchnxbir

Step	Hyp	Ref	Expression
1		xchnxbir.1	. 2
2		xchnxbir.2	. . 3
3	2	bicomi 202	. 2
4	1, 3	xchnxbi 308	1

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

This theorem is referenced by:  3ioran  991  nnelOLD  2803  nsspssun  3730  undif3  3758  ordtri3or  4915  intirr  5390  frxp  6910  ressuppssdif  6940  domunfican  7813  ssfin4  8711  wrdsymb0  12575  symgfix2  16441  gsumdixpOLD  17257  gsumdixp  17258  symgmatr01lem  19155  ppttop  19508  mdegleb  22464  strlem1  27169  isarchi  27726  dfon3  29542  dvtanlem  30064  ftc1anclem3  30092  2exanali  31293  bnj1189  34065  hdmaplem4  37501  mapdh9a  37517  bj-ifnot23  37718  bj-ifdfxor  37732

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