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  989  nanbi  1350  2nalexn  1629  2exnaln  1630  sbn  2105  ralnex  2910  rexnalOLD  2913  rexanali  2917  r2exlem  2982  nss  3562  difdif  3630  difab  3767  sbcnel12g  3826  ssdif0  3885  difin0ss  3893  disjsn  4088  iundif2  4392  iindif2  4394  notzfaus  4622  rexxfr  4667  nssss  4703  reldm0  5220  domtriord  7663  rnelfmlem  20216  dchrfi  23286  wwlknext  24428  brsymdif  29083  df3nandALT2  29468  dvasin  29708  wopprc  30604  lcvbr3  33838  cvrval2  34089
  Copyright terms: Public domain W3C validator