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  981  nanbi  1341  2nalexn  1620  2exnaln  1621  sbn  2091  ralnex  2848  rexnalOLD  2850  nss  3517  difdif  3585  difab  3722  sbcnel12g  3781  ssdif0  3840  difin0ss  3848  disjsn  4039  iundif2  4340  iindif2  4342  notzfaus  4570  rexxfr  4615  nssss  4651  reldm0  5160  domtriord  7562  rnelfmlem  19652  dchrfi  22722  brsymdif  27998  df3nandALT2  28383  dvasin  28623  wopprc  29522  wwlknext  30499  lcvbr3  32987  cvrval2  33238
  Copyright terms: Public domain W3C validator