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

Theorem xchbinxr 317
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 207 . 2  |-  ( ps  <->  ch )
41, 3xchbinx 316 1  |-  ( ph  <->  -. 
ch )
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    <-> wb 189
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 190
This theorem is referenced by:  3anor  1007  nanbiOLDOLD  1405  2nalexn  1711  2exnaln  1712  sbn  2231  ralnex  2846  rexanali  2852  r2exlem  2922  nss  3502  difdif  3571  difab  3724  sbcnel12g  3786  ssdif0  3835  difin0ss  3845  disjsn  4044  iundif2  4359  iindif2  4361  brsymdif  4473  notzfaus  4592  rexxfr  4634  nssss  4670  reldm0  5071  domtriord  7744  rnelfmlem  21016  dchrfi  24232  wwlknext  25501  df3nandALT2  31107  bj-ssbn  31299  poimirlem1  31986  dvasin  32073  lcvbr3  32634  cvrval2  32885  wopprc  35930  dfss6  36408
  Copyright terms: Public domain W3C validator