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

Theorem xchbinxr 312
Description: Replacement of a subexpression by an equivalent one. (Contributed by Wolf Lammen, 27-Sep-2014.)
Hypotheses
Ref Expression
xchbinxr.1  |-  ( ph  <->  -. 
ps )
xchbinxr.2  |-  ( ch  <->  ps )
Assertion
Ref Expression
xchbinxr  |-  ( ph  <->  -. 
ch )

Proof of Theorem xchbinxr
StepHypRef Expression
1 xchbinxr.1 . 2  |-  ( ph  <->  -. 
ps )
2 xchbinxr.2 . . 3  |-  ( ch  <->  ps )
32bicomi 205 . 2  |-  ( ps  <->  ch )
41, 3xchbinx 311 1  |-  ( ph  <->  -. 
ch )
Colors of variables: wff setvar class
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:  3anor  998  nanbiOLDOLD  1390  2nalexn  1696  2exnaln  1697  sbn  2186  ralnex  2878  rexnalOLD  2881  rexanali  2885  r2exlem  2955  nss  3528  difdif  3597  difab  3748  sbcnel12g  3808  ssdif0  3857  difin0ss  3867  disjsn  4063  iundif2  4369  iindif2  4371  brsymdif  4482  notzfaus  4600  rexxfr  4642  nssss  4678  reldm0  5072  domtriord  7724  rnelfmlem  20898  dchrfi  24046  wwlknext  25297  df3nandALT2  30843  poimirlem1  31645  dvasin  31732  lcvbr3  32298  cvrval2  32549  wopprc  35591  dfss6  36000
  Copyright terms: Public domain W3C validator