MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  xchbinxr Structured version   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  |-  ( 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 202 . 2  |-  ( ps  <->  ch )
41, 3xchbinx 310 1  |-  ( ph  <->  -. 
ch )
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    <-> wb 184
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
This theorem is referenced by:  3anor  976  nanbi  1335  2nalexn  1624  2exnaln  1625  sbn  2088  ralnex  2723  rexnal  2724  nss  3411  difdif  3479  difab  3616  sbcnel12g  3675  ssdif0  3734  difin0ss  3742  disjsn  3933  iundif2  4234  iindif2  4236  notzfaus  4464  rexxfr  4509  nssss  4545  reldm0  5053  domtriord  7453  rnelfmlem  19425  dchrfi  22537  brsymdif  27772  df3nandALT2  28157  dvasin  28389  wopprc  29288  wwlknext  30265  lcvbr3  32356  cvrval2  32607
  Copyright terms: Public domain W3C validator