Theorem xchbinxr 311

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

Hypotheses

Ref	Expression
xchbinxr.1
xchbinxr.2

Assertion

Ref	Expression
xchbinxr

Proof of Theorem xchbinxr

Step	Hyp	Ref	Expression
1		xchbinxr.1	. 2
2		xchbinxr.2	. . 3
3	2	bicomi 202	. 2
4	1, 3	xchbinx 310	1

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

This theorem is referenced by:  3anor  989  nanbiOLD  1353  2nalexn  1649  2exnaln  1650  sbn  2132  ralnex  2903  rexnalOLD  2906  rexanali  2910  r2exlem  2977  nss  3561  difdif  3629  difab  3766  sbcnel12g  3826  ssdif0  3885  difin0ss  3894  disjsn  4090  iundif2  4397  iindif2  4399  notzfaus  4627  rexxfr  4672  nssss  4708  reldm0  5225  domtriord  7683  rnelfmlem  20453  dchrfi  23530  wwlknext  24724  brsymdif  29478  df3nandALT2  29863  dvasin  30103  wopprc  30972  lcvbr3  34748  cvrval2  34999  dfss6  37792

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