Theorem pncand 11576

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 11470	. 2 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((𝐴 + 𝐵) − 𝐵) = 𝐴)
4	1, 2, 3	syl2anc 582	1 ⊢ (𝜑 → ((𝐴 + 𝐵) − 𝐵) = 𝐴)

Syntax hints:   → wi 4   = wceq 1539   ∈ wcel 2104  (class class class)co 7411  ℂcc 11110   + caddc 11115   − cmin 11448

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1911  ax-6 1969  ax-7 2009  ax-8 2106  ax-9 2114  ax-10 2135  ax-11 2152  ax-12 2169  ax-ext 2701  ax-sep 5298  ax-nul 5305  ax-pow 5362  ax-pr 5426  ax-un 7727  ax-resscn 11169  ax-1cn 11170  ax-icn 11171  ax-addcl 11172  ax-addrcl 11173  ax-mulcl 11174  ax-mulrcl 11175  ax-mulcom 11176  ax-addass 11177  ax-mulass 11178  ax-distr 11179  ax-i2m1 11180  ax-1ne0 11181  ax-1rid 11182  ax-rnegex 11183  ax-rrecex 11184  ax-cnre 11185  ax-pre-lttri 11186  ax-pre-lttrn 11187  ax-pre-ltadd 11188

This theorem depends on definitions:  df-bi 206  df-an 395  df-or 844  df-3or 1086  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2532  df-eu 2561  df-clab 2708  df-cleq 2722  df-clel 2808  df-nfc 2883  df-ne 2939  df-nel 3045  df-ral 3060  df-rex 3069  df-reu 3375  df-rab 3431  df-v 3474  df-sbc 3777  df-csb 3893  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-nul 4322  df-if 4528  df-pw 4603  df-sn 4628  df-pr 4630  df-op 4634  df-uni 4908  df-br 5148  df-opab 5210  df-mpt 5231  df-id 5573  df-po 5587  df-so 5588  df-xp 5681  df-rel 5682  df-cnv 5683  df-co 5684  df-dm 5685  df-rn 5686  df-res 5687  df-ima 5688  df-iota 6494  df-fun 6544  df-fn 6545  df-f 6546  df-f1 6547  df-fo 6548  df-f1o 6549  df-fv 6550  df-riota 7367  df-ov 7414  df-oprab 7415  df-mpo 7416  df-er 8705  df-en 8942  df-dom 8943  df-sdom 8944  df-pnf 11254  df-mnf 11255  df-ltxr 11257  df-sub 11450

This theorem is referenced by:  mvlraddd  11628  mvlladdd  11629  mvrraddd  11630  addlsub  11634  pnpncand  11639  pncan1  11642  eluzmn  12833  icoshftf1o  13455  xov1plusxeqvd  13479  zesq  14193  hashdifsnp1  14461  ccatval3  14533  fsump1  15706  fsumrev2  15732  fprodp1  15917  risefacp1  15977  fallfacp1  15978  sadcp1  16400  smupp1  16425  hashdvds  16712  pythagtriplem4  16756  pythagtriplem6  16758  pythagtriplem7  16759  pythagtriplem12  16763  pythagtriplem14  16765  pcqdiv  16794  mulgdirlem  19021  cayhamlem1  22588  pjthlem1  25185  ovolicopnf  25273  i1faddlem  25442  itg1addlem4  25448  itg1addlem4OLD  25449  itgpowd  25802  taylthlem2  26122  ulmshft  26138  efif1olem2  26288  efif1olem4  26290  logdiflbnd  26735  lgamgulmlem2  26770  lgamcvg2  26795  relgamcl  26802  ftalem2  26814  mulog2sumlem1  27273  mulog2sumlem3  27275  pntrlog2bndlem2  27317  pntrlog2bndlem4  27319  pntrlog2bndlem5  27320  colinearalglem4  28434  axpaschlem  28465  wwlksnred  29413  wwlksnext  29414  wwlksnredwwlkn  29416  wwlksnextproplem2  29431  clwlkclwwlklem2  29520  clwlkclwwlklem3  29521  clwwlkf  29567  wwlksext2clwwlk  29577  eucrct2eupth  29765  numclwwlk2lem1  29896  numclwlk2lem2f  29897  pjhthlem1  30911  fzm1ne1  32267  fzom1ne1  32279  wrdt2ind  32384  cshwrnid  32392  psgnfzto1stlem  32529  cycpmco2lem4  32558  cycpmco2lem5  32559  cycpmco2lem7  32561  madjusmdetlem2  33106  dya2icoseg  33574  fibp1  33698  ballotlemfc0  33789  ballotlemfcc  33790  ballotlemsgt1  33807  ballotlemsel1i  33809  ballotlemsima  33812  ballotlem1ri  33831  signstfvn  33878  reprsuc  33925  bcprod  35012  bccolsum  35013  unblimceq0  35686  knoppndvlem6  35696  bj-bary1lem1  36495  sin2h  36781  itg2addnclem  36842  itg2addnclem3  36844  areacirclem4  36882  ssbnd  36959  lcmineqlem10  41209  lcmineqlem11  41210  lcmineqlem18  41217  lcmineqlem19  41218  sticksstones12a  41279  sticksstones12  41280  metakunt12  41302  mvrrsubd  41489  fz1sump1  41510  oddnumth  41511  dffltz  41678  jm2.19lem4  42033  jm2.23  42037  int-eqmvtd  43243  hashnzfzclim  43383  dvradcnv2  43408  binomcxplemnn0  43410  binomcxplemnotnn0  43417  nnsplit  44366  iccshift  44529  iooshift  44533  climinf  44620  limcperiod  44642  0ellimcdiv  44663  cncfshift  44888  cncfperiod  44893  dvdsn1add  44953  dvnmul  44957  dvnprodlem1  44960  itgiccshift  44994  itgperiod  44995  stoweidlem17  45031  wallispilem4  45082  wallispilem5  45083  stirlinglem1  45088  stirlinglem5  45092  stirlinglem6  45093  stirlinglem10  45097  dirkertrigeqlem2  45113  fourierdlem14  45135  fourierdlem19  45140  fourierdlem41  45162  fourierdlem42  45163  fourierdlem48  45168  fourierdlem49  45169  fourierdlem50  45170  fourierdlem64  45184  fourierdlem74  45194  fourierdlem75  45195  fourierdlem81  45201  fourierdlem92  45212  fourierdlem97  45217  fourierdlem103  45223  fourierdlem104  45224  fourierdlem107  45227  etransclem9  45257  nnfoctbdjlem  45469  fldivmod  47291