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

Theorem negeqd 9300
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 9298 . 2  |-  ( A  =  B  ->  -u A  =  -u B )
31, 2syl 16 1  |-  ( ph  -> 
-u A  =  -u B )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1652   -ucneg 9292
This theorem is referenced by:  negdi  9358  mulneg2  9471  mulm1  9475  ltord2  9556  leord2  9557  eqord2  9558  divneg  9709  div2neg  9737  recgt0  9854  infmsup  9986  supminf  10563  modcyc2  11277  monoord2  11354  expval  11384  discr  11516  reneg  11930  imneg  11938  cjcj  11945  cjneg  11952  sqeqd  11971  fsumtscopo2  12582  infcvgaux1i  12636  infcvgaux2i  12637  sinneg  12747  tanneg  12749  sincossq  12777  odd2np1  12908  oexpneg  12911  modgcd  13036  pcneg  13247  mulgval  14892  mulgneg  14908  evth2  18985  ivth2  19352  mbfposb  19545  mbfinf  19557  mbfi1flimlem  19614  iblcnlem  19680  iblrelem  19682  itgrevallem1  19686  iblneg  19694  itgneg  19695  ibladd  19712  ditgeq1  19735  ditgeq2  19736  ditgeq3  19737  ditgneg  19744  ditgswap  19746  dvrec  19841  dvexp3  19862  dvsincos  19865  rolle  19874  dvivth  19894  dvfsumge  19906  dvfsumlem2  19911  dvfsum2  19918  ftc2ditg  19930  vieta1lem2  20228  vieta1  20229  aaliou3lem2  20260  aaliou3lem8  20262  aaliou3lem5  20264  aaliou3lem6  20265  aaliou3lem7  20266  aaliou3  20268  sinperlem  20388  efimpi  20399  ptolemy  20404  sineq0  20429  efeq1  20431  tanregt0  20441  efif1olem2  20445  lognegb  20484  logneg2  20510  advlogexp  20546  logtayl  20551  logtayl2  20553  logccv  20554  cxpmul2z  20582  cosangneg2d  20649  isosctrlem2  20663  isosctrlem3  20664  angpined  20671  dcubic1lem  20683  dcubic2  20684  mcubic  20687  cubic2  20688  dquart  20693  quart1lem  20695  quartlem1  20697  quart  20701  asinlem3a  20710  asinneg  20726  atanneg  20747  atancj  20750  atanlogaddlem  20753  atanlogsublem  20755  atantan  20763  atantayl  20777  birthdaylem3  20792  amgmlem  20828  emcllem7  20840  ftalem5  20859  basellem5  20867  basellem9  20871  lgsneg1  21104  lgseisenlem1  21133  lgseisenlem4  21136  m1lgs  21146  2sqblem  21161  dchrisum0flblem1  21202  rpvmasum2  21206  pntrsumo1  21259  pntrlog2bndlem2  21272  pntibndlem2  21285  padicfval  21310  padicval  21311  ostth3  21332  nvabs  22162  ipasslem2  22333  numdenneg  24160  xrge0iifcv  24320  xrge0iifhom  24323  xrge0iif1  24324  xrge0tmdOLD  24331  xrge0tmd  24332  logbrec  24405  lgamgulmlem2  24814  climlec3  25214  risefallfac  25340  brbtwn2  25844  colinearalglem4  25848  axsegconlem9  25864  bpoly3  26104  itg2addnclem3  26258  ibladdnc  26262  ftc1anclem5  26284  ftc1anclem6  26285  areacirclem1  26292  areacirc  26297  pellexlem6  26897  pell1234qrdich  26924  rmxm1  26997  rmym1  26998  monotoddzzfi  27005  monotoddzz  27006  oddcomabszz  27007  acongeq12d  27044  acongeq  27048  psgnunilem2  27395  itgsin0pilem1  27720  itgsinexplem1  27724  stoweidlem13  27738  stirlinglem5  27803  sigarac  27818  sigaras  27821  sigarms  27822  sigariz  27829  sigarcol  27830  sharhght  27831  sigaradd  27832  ceilingval  28528  sineq0ALT  29049
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-6 1744  ax-7 1749  ax-11 1761  ax-12 1950  ax-ext 2417
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3an 938  df-tru 1328  df-ex 1551  df-nf 1554  df-sb 1659  df-clab 2423  df-cleq 2429  df-clel 2432  df-nfc 2561  df-rex 2711  df-rab 2714  df-v 2958  df-dif 3323  df-un 3325  df-in 3327  df-ss 3334  df-nul 3629  df-if 3740  df-sn 3820  df-pr 3821  df-op 3823  df-uni 4016  df-br 4213  df-iota 5418  df-fv 5462  df-ov 6084  df-neg 9294
  Copyright terms: Public domain W3C validator