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  1694  2exnaln  1695  sbn  2190  ralnex  2805  rexanali  2811  r2exlem  2881  nss  3458  difdif  3527  difab  3678  sbcnel12g  3740  ssdif0  3789  difin0ss  3799  disjsn  3996  iundif2  4302  iindif2  4304  brsymdif  4416  notzfaus  4535  rexxfr  4577  nssss  4613  reldm0  5007  domtriord  7664  rnelfmlem  20902  dchrfi  24118  wwlknext  25387  df3nandALT2  31000  poimirlem1  31842  dvasin  31929  lcvbr3  32495  cvrval2  32746  wopprc  35792  dfss6  36270
  Copyright terms: Public domain W3C validator