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

Theorem negeqd 9046
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 9044 . 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 1623   -ucneg 9038
This theorem is referenced by:  negdi  9104  mulneg2  9217  mulm1  9221  ltord2  9302  leord2  9303  eqord2  9304  divneg  9455  div2neg  9483  recgt0  9600  infmsup  9732  supminf  10305  modcyc2  11000  monoord2  11077  expval  11106  discr  11238  reneg  11610  imneg  11618  cjcj  11625  cjneg  11632  sqeqd  11651  fsumtscopo2  12261  infcvgaux1i  12315  infcvgaux2i  12316  sinneg  12426  tanneg  12428  sincossq  12456  odd2np1  12587  oexpneg  12590  modgcd  12715  pcneg  12926  mulgval  14569  mulgneg  14585  evth2  18458  ivth2  18815  mbfposb  19008  mbfinf  19020  mbfi1flimlem  19077  iblcnlem  19143  iblrelem  19145  itgrevallem1  19149  iblneg  19157  itgneg  19158  ibladd  19175  ditgeq1  19198  ditgeq2  19199  ditgeq3  19200  ditgneg  19207  ditgswap  19209  dvrec  19304  dvexp3  19325  dvsincos  19328  rolle  19337  dvivth  19357  dvfsumge  19369  dvfsumlem2  19374  dvfsum2  19381  ftc2ditg  19393  vieta1lem2  19691  vieta1  19692  aaliou3lem2  19723  aaliou3lem8  19725  aaliou3lem5  19727  aaliou3lem6  19728  aaliou3lem7  19729  aaliou3  19731  sinperlem  19848  efimpi  19859  ptolemy  19864  sineq0  19889  efeq1  19891  tanregt0  19901  efif1olem2  19905  lognegb  19943  logneg2  19969  advlogexp  20002  logtayl  20007  logtayl2  20009  logccv  20010  cxpmul2z  20038  cosangneg2d  20105  isosctrlem2  20119  isosctrlem3  20120  angpined  20127  dcubic1lem  20139  dcubic2  20140  mcubic  20143  cubic2  20144  dquart  20149  quart1lem  20151  quartlem1  20153  quart  20157  asinlem3a  20166  asinneg  20182  atanneg  20203  atancj  20206  atanlogaddlem  20209  atanlogsublem  20211  atantan  20219  atantayl  20233  birthdaylem3  20248  amgmlem  20284  emcllem7  20295  ftalem5  20314  basellem5  20322  basellem9  20326  lgsneg1  20559  lgseisenlem1  20588  lgseisenlem4  20591  m1lgs  20601  2sqblem  20616  dchrisum0flblem1  20657  rpvmasum2  20661  pntrsumo1  20714  pntrlog2bndlem2  20727  pntibndlem2  20740  padicfval  20765  padicval  20766  ostth3  20787  nvabs  21239  ipasslem2  21410  xrge0iifcv  23316  xrge0iifhom  23319  xrge0iif1  23320  xrge0tmdALT  23327  xrge0tmd  23328  logbrec  23407  brbtwn2  24533  colinearalglem4  24537  axsegconlem9  24553  bpoly3  24793  areacirclem2  24925  areacirc  24931  pellexlem6  26919  pell1234qrdich  26946  rmxm1  27019  rmym1  27020  monotoddzzfi  27027  monotoddzz  27028  oddcomabszz  27029  acongeq12d  27066  acongeq  27070  psgnunilem2  27418  itgsin0pilem1  27744  itgsinexplem1  27748  stoweidlem13  27762  stirlinglem5  27827  sigarac  27842  sigaras  27845  sigarms  27846  sigariz  27853  sigarcol  27854  sharhght  27855  sigaradd  27856  ceilingval  28255
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3an 936  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-clab 2270  df-cleq 2276  df-clel 2279  df-nfc 2408  df-rex 2549  df-rab 2552  df-v 2790  df-dif 3155  df-un 3157  df-in 3159  df-ss 3166  df-nul 3456  df-if 3566  df-sn 3646  df-pr 3647  df-op 3649  df-uni 3828  df-br 4024  df-iota 5219  df-fv 5263  df-ov 5861  df-neg 9040
  Copyright terms: Public domain W3C validator