MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  xchbinxr Unicode version

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
StepHypRef Expression
1 xchbinxr.1 . 2
2 xchbinxr.2 . . 3
32bicomi 202 . 2
41, 3xchbinx 310 1
Colors of variables: wff setvar class
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
  Copyright terms: Public domain W3C validator