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

Theorem negeqd 9091
Description: Equality deduction for negatives. (Contributed by NM, 14-May-1999.)
Hypothesis
Ref Expression
negeqd.1  |-  ( ph  ->  A  =  B )
Assertion
Ref Expression
negeqd  |-  ( ph  -> 
-u A  =  -u B )

Proof of Theorem negeqd
StepHypRef Expression
1 negeqd.1 . 2  |-  ( ph  ->  A  =  B )
2 negeq 9089 . 2  |-  ( A  =  B  ->  -u A  =  -u B )
31, 2syl 15 1  |-  ( ph  -> 
-u A  =  -u B )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1633   -ucneg 9083
This theorem is referenced by:  negdi  9149  mulneg2  9262  mulm1  9266  ltord2  9347  leord2  9348  eqord2  9349  divneg  9500  div2neg  9528  recgt0  9645  infmsup  9777  supminf  10352  modcyc2  11047  monoord2  11124  expval  11153  discr  11285  reneg  11657  imneg  11665  cjcj  11672  cjneg  11679  sqeqd  11698  fsumtscopo2  12308  infcvgaux1i  12362  infcvgaux2i  12363  sinneg  12473  tanneg  12475  sincossq  12503  odd2np1  12634  oexpneg  12637  modgcd  12762  pcneg  12973  mulgval  14618  mulgneg  14634  evth2  18511  ivth2  18868  mbfposb  19061  mbfinf  19073  mbfi1flimlem  19130  iblcnlem  19196  iblrelem  19198  itgrevallem1  19202  iblneg  19210  itgneg  19211  ibladd  19228  ditgeq1  19251  ditgeq2  19252  ditgeq3  19253  ditgneg  19260  ditgswap  19262  dvrec  19357  dvexp3  19378  dvsincos  19381  rolle  19390  dvivth  19410  dvfsumge  19422  dvfsumlem2  19427  dvfsum2  19434  ftc2ditg  19446  vieta1lem2  19744  vieta1  19745  aaliou3lem2  19776  aaliou3lem8  19778  aaliou3lem5  19780  aaliou3lem6  19781  aaliou3lem7  19782  aaliou3  19784  sinperlem  19901  efimpi  19912  ptolemy  19917  sineq0  19942  efeq1  19944  tanregt0  19954  efif1olem2  19958  lognegb  19996  logneg2  20022  advlogexp  20055  logtayl  20060  logtayl2  20062  logccv  20063  cxpmul2z  20091  cosangneg2d  20158  isosctrlem2  20172  isosctrlem3  20173  angpined  20180  dcubic1lem  20192  dcubic2  20193  mcubic  20196  cubic2  20197  dquart  20202  quart1lem  20204  quartlem1  20206  quart  20210  asinlem3a  20219  asinneg  20235  atanneg  20256  atancj  20259  atanlogaddlem  20262  atanlogsublem  20264  atantan  20272  atantayl  20286  birthdaylem3  20301  amgmlem  20337  emcllem7  20348  ftalem5  20367  basellem5  20375  basellem9  20379  lgsneg1  20612  lgseisenlem1  20641  lgseisenlem4  20644  m1lgs  20654  2sqblem  20669  dchrisum0flblem1  20710  rpvmasum2  20714  pntrsumo1  20767  pntrlog2bndlem2  20780  pntibndlem2  20793  padicfval  20818  padicval  20819  ostth3  20840  nvabs  21294  ipasslem2  21465  numdenneg  23312  xrge0iifcv  23389  xrge0iifhom  23392  xrge0iif1  23393  xrge0tmdALT  23400  xrge0tmd  23401  logbrec  23597  brbtwn2  24919  colinearalglem4  24923  axsegconlem9  24939  bpoly3  25179  itg2addnc  25319  ibladdnc  25322  areacirclem2  25342  areacirc  25348  pellexlem6  26067  pell1234qrdich  26094  rmxm1  26167  rmym1  26168  monotoddzzfi  26175  monotoddzz  26176  oddcomabszz  26177  acongeq12d  26214  acongeq  26218  psgnunilem2  26566  itgsin0pilem1  26892  itgsinexplem1  26896  stoweidlem13  26910  stirlinglem5  26975  sigarac  26990  sigaras  26993  sigarms  26994  sigariz  27001  sigarcol  27002  sharhght  27003  sigaradd  27004  ceilingval  27704
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1537  ax-5 1548  ax-17 1607  ax-9 1645  ax-8 1666  ax-6 1720  ax-7 1725  ax-11 1732  ax-12 1897  ax-ext 2297
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3an 936  df-tru 1310  df-ex 1533  df-nf 1536  df-sb 1640  df-clab 2303  df-cleq 2309  df-clel 2312  df-nfc 2441  df-rex 2583  df-rab 2586  df-v 2824  df-dif 3189  df-un 3191  df-in 3193  df-ss 3200  df-nul 3490  df-if 3600  df-sn 3680  df-pr 3681  df-op 3683  df-uni 3865  df-br 4061  df-iota 5256  df-fv 5300  df-ov 5903  df-neg 9085
  Copyright terms: Public domain W3C validator