Theorem pncand 11588

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

Step	Hyp	Ref	Expression
1		negidd.1	. 2 ⊢ (𝜑 → 𝐴 ∈ ℂ)
2		pncand.2	. 2 ⊢ (𝜑 → 𝐵 ∈ ℂ)
3		pncan 11481	. 2 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((𝐴 + 𝐵) − 𝐵) = 𝐴)
4	1, 2, 3	syl2anc 596	1 ⊢ (𝜑 → ((𝐴 + 𝐵) − 𝐵) = 𝐴)

This proof depends on syntax axioms:   → wi 4   = wceq 1570   ∈ wcel 2146  (class class class)co 7423  ℂcc 11116   + caddc 11121   − cmin 11459

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-10 2179  ax-11 2195  ax-12 2216  ax-ext 2738  ax-sep 5262  ax-nul 5274  ax-pow 5341  ax-pr 5409  ax-un 7745  ax-resscn 11175  ax-1cn 11176  ax-icn 11177  ax-addcl 11178  ax-addrcl 11179  ax-mulcl 11180  ax-mulrcl 11181  ax-mulcom 11182  ax-addass 11183  ax-mulass 11184  ax-distr 11185  ax-i2m1 11186  ax-1ne0 11187  ax-1rid 11188  ax-rnegex 11189  ax-rrecex 11190  ax-cnre 11191  ax-pre-lttri 11192  ax-pre-lttrn 11193  ax-pre-ltadd 11194

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2100  df-mo 2570  df-eu 2600  df-clab 2745  df-cleq 2758  df-clel 2841  df-nfc 2915  df-ne 2962  df-nel 3068  df-ral 3083  df-rex 3093  df-reu 3373  df-rab 3420  df-v 3460  df-sbc 3748  df-csb 3857  df-dif 3911  df-un 3913  df-in 3915  df-ss 3925  df-nul 4290  df-if 4493  df-pw 4569  df-sn 4595  df-pr 4597  df-op 4601  df-uni 4878  df-br 5115  df-opab 5179  df-mpt 5198  df-id 5561  df-po 5574  df-so 5575  df-xp 5672  df-rel 5673  df-cnv 5674  df-co 5675  df-dm 5676  df-rn 5677  df-res 5678  df-ima 5679  df-iota 6499  df-fun 6545  df-fn 6546  df-f 6547  df-f1 6548  df-fo 6549  df-f1o 6550  df-fv 6551  df-riota 7380  df-ov 7426  df-oprab 7427  df-mpo 7428  df-er 8703  df-en 8953  df-dom 8954  df-sdom 8955  df-pnf 11263  df-mnf 11264  df-ltxr 11266  df-sub 11461

This theorem is used by:  mvlraddd  11642  mvlladdd  11643  mvrraddd  11644  addlsub  11648  pnpncand  11653  pncan1  11656  eluzmn  12887  icoshftf1o  13519  xov1plusxeqvd  13543  fzom1ne1  13833  modaddb  13962  zesq  14282  hashdifsnp1  14563  ccatval3  14636  fsump1  15833  fsumrev2  15859  fprodp1  16049  risefacp1  16108  fallfacp1  16109  sadcp1  16538  smupp1  16563  hashdvds  16859  pythagtriplem4  16904  pythagtriplem6  16906  pythagtriplem7  16907  pythagtriplem12  16911  pythagtriplem14  16913  pcqdiv  16942  chnub  18703  chnlt  18704  chnccat  18707  mulgdirlem  19202  psdmplcl  22362  cayhamlem1  23060  pjthlem1  25633  ovolicopnf  25720  i1faddlem  25889  itg1addlem4  25895  itgpowd  26246  taylthlem2  26574  ulmshft  26590  efif1olem2  26745  efif1olem4  26747  logdiflbnd  27196  lgamgulmlem2  27231  lgamcvg2  27256  relgamcl  27263  ftalem2  27275  mulog2sumlem1  27735  mulog2sumlem3  27737  pntrlog2bndlem2  27779  pntrlog2bndlem4  27781  pntrlog2bndlem5  27782  colinearalglem4  29296  axpaschlem  29327  wwlksnred  30278  wwlksnext  30279  wwlksnredwwlkn  30281  wwlksnextproplem2  30296  clwlkclwwlklem2  30388  clwlkclwwlklem3  30389  clwwlkf  30435  wwlksext2clwwlk  30445  eucrct2eupth  30633  numclwwlk2lem1  30764  numclwlk2lem2f  30765  pjhthlem1  31780  fzm1ne1  33170  wrdt2ind  33306  cshwrnid  33312  psgnfzto1stlem  33451  cycpmco2lem4  33480  cycpmco2lem5  33481  cycpmco2lem7  33483  esplyindfv  33997  constraddcl  34183  constrremulcl  34188  madjusmdetlem2  34249  dya2icoseg  34699  fibp1  34823  ballotlemfc0  34915  ballotlemfcc  34916  ballotlemsgt1  34933  ballotlemsel1i  34935  ballotlemsima  34938  ballotlem1ri  34957  signstfvn  34988  reprsuc  35034  bcprod  36251  bccolsum  36252  unblimceq0  37137  knoppndvlem6  37147  bj-bary1lem1  37996  sin2h  38302  itg2addnclem  38363  itg2addnclem3  38365  areacirclem4  38403  ssbnd  38480  lcmineqlem10  42846  lcmineqlem11  42847  lcmineqlem18  42854  lcmineqlem19  42855  sticksstones12a  42965  sticksstones12  42966  aks6d1c6lem3  42980  bcle2d  42987  aks6d1c7lem1  42988  mvrrsubd  43076  fz1sump1  43112  oddnumth  43113  dffltz  43407  jm2.19lem4  43760  jm2.23  43764  int-eqmvtd  44956  hashnzfzclim  45073  dvradcnv2  45098  binomcxplemnn0  45100  binomcxplemnotnn0  45107  nnsplit  46115  iccshift  46275  iooshift  46279  climinf  46363  limcperiod  46385  0ellimcdiv  46404  cncfshift  46629  cncfperiod  46634  dvdsn1add  46694  dvnmul  46698  itgiccshift  46735  itgperiod  46736  stoweidlem17  46772  wallispilem4  46823  wallispilem5  46824  stirlinglem1  46829  stirlinglem5  46833  stirlinglem6  46834  stirlinglem10  46838  dirkertrigeqlem2  46854  fourierdlem14  46876  fourierdlem19  46881  fourierdlem41  46903  fourierdlem42  46904  fourierdlem48  46909  fourierdlem49  46910  fourierdlem50  46911  fourierdlem64  46925  fourierdlem74  46935  fourierdlem75  46936  fourierdlem81  46942  fourierdlem92  46953  fourierdlem97  46958  fourierdlem103  46964  fourierdlem104  46965  fourierdlem107  46968  etransclem9  46998  nnfoctbdjlem  47210  chnerlem2  47640  fldivmod  48122  gpgvtxedg1  48870