MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  pncand Structured version   Visualization version   GIF version

Theorem pncand 10244
Description: Cancellation law for subtraction. (Contributed by Mario Carneiro, 27-May-2016.)
Hypotheses
Ref Expression
negidd.1 (𝜑𝐴 ∈ ℂ)
pncand.2 (𝜑𝐵 ∈ ℂ)
Assertion
Ref Expression
pncand (𝜑 → ((𝐴 + 𝐵) − 𝐵) = 𝐴)

Proof of Theorem pncand
StepHypRef Expression
1 negidd.1 . 2 (𝜑𝐴 ∈ ℂ)
2 pncand.2 . 2 (𝜑𝐵 ∈ ℂ)
3 pncan 10138 . 2 ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((𝐴 + 𝐵) − 𝐵) = 𝐴)
41, 2, 3syl2anc 690 1 (𝜑 → ((𝐴 + 𝐵) − 𝐵) = 𝐴)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1474  wcel 1976  (class class class)co 6527  cc 9790   + caddc 9795  cmin 10117
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-5 1826  ax-6 1874  ax-7 1921  ax-8 1978  ax-9 1985  ax-10 2005  ax-11 2020  ax-12 2032  ax-13 2232  ax-ext 2589  ax-sep 4703  ax-nul 4712  ax-pow 4764  ax-pr 4828  ax-un 6824  ax-resscn 9849  ax-1cn 9850  ax-icn 9851  ax-addcl 9852  ax-addrcl 9853  ax-mulcl 9854  ax-mulrcl 9855  ax-mulcom 9856  ax-addass 9857  ax-mulass 9858  ax-distr 9859  ax-i2m1 9860  ax-1ne0 9861  ax-1rid 9862  ax-rnegex 9863  ax-rrecex 9864  ax-cnre 9865  ax-pre-lttri 9866  ax-pre-lttrn 9867  ax-pre-ltadd 9868
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-3or 1031  df-3an 1032  df-tru 1477  df-ex 1695  df-nf 1700  df-sb 1867  df-eu 2461  df-mo 2462  df-clab 2596  df-cleq 2602  df-clel 2605  df-nfc 2739  df-ne 2781  df-nel 2782  df-ral 2900  df-rex 2901  df-reu 2902  df-rab 2904  df-v 3174  df-sbc 3402  df-csb 3499  df-dif 3542  df-un 3544  df-in 3546  df-ss 3553  df-nul 3874  df-if 4036  df-pw 4109  df-sn 4125  df-pr 4127  df-op 4131  df-uni 4367  df-br 4578  df-opab 4638  df-mpt 4639  df-id 4943  df-po 4949  df-so 4950  df-xp 5034  df-rel 5035  df-cnv 5036  df-co 5037  df-dm 5038  df-rn 5039  df-res 5040  df-ima 5041  df-iota 5754  df-fun 5792  df-fn 5793  df-f 5794  df-f1 5795  df-fo 5796  df-f1o 5797  df-fv 5798  df-riota 6489  df-ov 6530  df-oprab 6531  df-mpt2 6532  df-er 7606  df-en 7819  df-dom 7820  df-sdom 7821  df-pnf 9932  df-mnf 9933  df-ltxr 9935  df-sub 10119
This theorem is referenced by:  mvlraddd  10295  mvrraddd  10296  addlsub  10298  pnpncand  10303  pncan1  10305  eluzmn  11526  icoshftf1o  12122  xov1plusxeqvd  12145  zesq  12804  brfi1indlem  13079  ccatval3  13162  fsumrev2  14302  binom1dif  14350  fprodp1  14484  risefacp1  14545  fallfacp1  14546  bpolydiflem  14570  sadcp1  14961  smupp1  14986  hashdvds  15264  pythagtriplem4  15308  pythagtriplem6  15310  pythagtriplem7  15311  pythagtriplem12  15315  pythagtriplem14  15317  pcqdiv  15346  mulgdirlem  17341  cayhamlem1  20432  blhalf  21961  pjthlem1  22933  ovolicopnf  23016  i1faddlem  23183  itg1addlem4  23189  ftc1lem4  23523  aaliou3lem8  23821  taylthlem2  23849  ulmshft  23865  efif1olem2  24010  efif1olem4  24012  quart1lem  24299  asinsin  24336  efiatan2  24361  logdiflbnd  24438  harmonicbnd4  24454  lgamgulmlem2  24473  lgamcvg2  24498  relgamcl  24505  ftalem1  24516  ftalem2  24517  bcctr  24717  pcbcctr  24718  bcp1ctr  24721  2sqblem  24873  mulog2sumlem1  24940  mulog2sumlem3  24942  pntrlog2bndlem2  24984  pntrlog2bndlem4  24986  pntrlog2bndlem5  24987  pntrlog2bndlem6  24989  colinearalglem4  25507  axpaschlem  25538  wwlknimp  25981  wwlknred  26017  wwlknredwwlkn  26020  wwlkextproplem2  26036  clwlkisclwwlklem1  26081  clwlkisclwwlklem0  26082  clwwlkf  26088  wwlkext2clwwlk  26097  rusgra0edg  26248  eupatrl  26261  numclwwlk2lem1  26395  numclwlk2lem2f  26396  pjhthlem1  27440  psgnfzto1stlem  28987  madjusmdetlem2  29028  dya2icoseg  29472  iwrdsplit  29582  fibp1  29596  ballotlemfc0  29687  ballotlemfcc  29688  ballotlemsgt1  29705  ballotlemsel1i  29707  ballotlemsima  29710  ballotlem1ri  29729  signstfvn  29778  bcprod  30683  bccolsum  30684  unblimceq0  31474  knoppndvlem6  31484  bj-bary1lem1  32141  sin2h  32372  itg2addnclem  32434  itg2addnclem3  32436  ftc1cnnclem  32456  areacirclem4  32476  ssbnd  32560  jm2.19lem4  36380  jm2.23  36384  jm3.1lem1  36405  itgpowd  36622  int-eqmvtd  37317  hashnzfzclim  37346  dvradcnv2  37371  binomcxplemnn0  37373  binomcxplemnotnn0  37380  nnsplit  38319  iccshift  38395  iooshift  38399  climinf  38477  limcperiod  38499  0ellimcdiv  38520  cncfshift  38563  cncfperiod  38568  dvdsn1add  38633  dvnmul  38637  dvnprodlem1  38640  itgiccshift  38676  itgperiod  38677  stoweidlem17  38714  wallispilem4  38765  wallispilem5  38766  stirlinglem1  38771  stirlinglem5  38775  stirlinglem6  38776  stirlinglem10  38780  dirkertrigeqlem2  38796  fourierdlem14  38818  fourierdlem19  38823  fourierdlem41  38845  fourierdlem42  38846  fourierdlem48  38851  fourierdlem49  38852  fourierdlem50  38853  fourierdlem64  38867  fourierdlem74  38877  fourierdlem75  38878  fourierdlem81  38884  fourierdlem92  38895  fourierdlem97  38900  fourierdlem103  38906  fourierdlem104  38907  fourierdlem107  38910  etransclem9  38940  nnfoctbdjlem  39152  wwlksnred  41100  wwlksnredwwlkn  41103  wwlksnextproplem2  41118  clwlkclwwlklem2  41211  clwlkclwwlklem3  41212  clwwlksf  41224  wwlksext2clwwlk  41233  eucrct2eupth  41415  av-numclwwlk2lem1  41534  av-numclwlk2lem2f  41535  fldivmod  42109  mvlladdd  42285  mvrladdd  42287
  Copyright terms: Public domain W3C validator