Theorem pncand 11316

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

Syntax hints:   → wi 4   = wceq 1541   ∈ wcel 2109  (class class class)co 7268  ℂcc 10853   + caddc 10858   − cmin 11188

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1801  ax-4 1815  ax-5 1916  ax-6 1974  ax-7 2014  ax-8 2111  ax-9 2119  ax-10 2140  ax-11 2157  ax-12 2174  ax-ext 2710  ax-sep 5226  ax-nul 5233  ax-pow 5291  ax-pr 5355  ax-un 7579  ax-resscn 10912  ax-1cn 10913  ax-icn 10914  ax-addcl 10915  ax-addrcl 10916  ax-mulcl 10917  ax-mulrcl 10918  ax-mulcom 10919  ax-addass 10920  ax-mulass 10921  ax-distr 10922  ax-i2m1 10923  ax-1ne0 10924  ax-1rid 10925  ax-rnegex 10926  ax-rrecex 10927  ax-cnre 10928  ax-pre-lttri 10929  ax-pre-lttrn 10930  ax-pre-ltadd 10931

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-3or 1086  df-3an 1087  df-tru 1544  df-fal 1554  df-ex 1786  df-nf 1790  df-sb 2071  df-mo 2541  df-eu 2570  df-clab 2717  df-cleq 2731  df-clel 2817  df-nfc 2890  df-ne 2945  df-nel 3051  df-ral 3070  df-rex 3071  df-reu 3072  df-rab 3074  df-v 3432  df-sbc 3720  df-csb 3837  df-dif 3894  df-un 3896  df-in 3898  df-ss 3908  df-nul 4262  df-if 4465  df-pw 4540  df-sn 4567  df-pr 4569  df-op 4573  df-uni 4845  df-br 5079  df-opab 5141  df-mpt 5162  df-id 5488  df-po 5502  df-so 5503  df-xp 5594  df-rel 5595  df-cnv 5596  df-co 5597  df-dm 5598  df-rn 5599  df-res 5600  df-ima 5601  df-iota 6388  df-fun 6432  df-fn 6433  df-f 6434  df-f1 6435  df-fo 6436  df-f1o 6437  df-fv 6438  df-riota 7225  df-ov 7271  df-oprab 7272  df-mpo 7273  df-er 8472  df-en 8708  df-dom 8709  df-sdom 8710  df-pnf 10995  df-mnf 10996  df-ltxr 10998  df-sub 11190

This theorem is referenced by:  mvlraddd  11368  mvlladdd  11369  mvrraddd  11370  addlsub  11374  pnpncand  11379  pncan1  11382  eluzmn  12571  icoshftf1o  13188  xov1plusxeqvd  13212  zesq  13922  hashdifsnp1  14191  ccatval3  14265  fsumrev2  15475  fprodp1  15660  risefacp1  15720  fallfacp1  15721  sadcp1  16143  smupp1  16168  hashdvds  16457  pythagtriplem4  16501  pythagtriplem6  16503  pythagtriplem7  16504  pythagtriplem12  16508  pythagtriplem14  16510  pcqdiv  16539  mulgdirlem  18715  cayhamlem1  21996  pjthlem1  24582  ovolicopnf  24669  i1faddlem  24838  itg1addlem4  24844  itg1addlem4OLD  24845  itgpowd  25195  taylthlem2  25514  ulmshft  25530  efif1olem2  25680  efif1olem4  25682  logdiflbnd  26125  lgamgulmlem2  26160  lgamcvg2  26185  relgamcl  26192  ftalem2  26204  mulog2sumlem1  26663  mulog2sumlem3  26665  pntrlog2bndlem2  26707  pntrlog2bndlem4  26709  pntrlog2bndlem5  26710  colinearalglem4  27258  axpaschlem  27289  wwlksnred  28236  wwlksnext  28237  wwlksnredwwlkn  28239  wwlksnextproplem2  28254  clwlkclwwlklem2  28343  clwlkclwwlklem3  28344  clwwlkf  28390  wwlksext2clwwlk  28400  eucrct2eupth  28588  numclwwlk2lem1  28719  numclwlk2lem2f  28720  pjhthlem1  29732  fzm1ne1  31089  fzom1ne1  31101  wrdt2ind  31204  cshwrnid  31212  psgnfzto1stlem  31346  cycpmco2lem4  31375  cycpmco2lem5  31376  cycpmco2lem7  31378  madjusmdetlem2  31757  dya2icoseg  32223  fibp1  32347  ballotlemfc0  32438  ballotlemfcc  32439  ballotlemsgt1  32456  ballotlemsel1i  32458  ballotlemsima  32461  ballotlem1ri  32480  signstfvn  32527  reprsuc  32574  bcprod  33683  bccolsum  33684  unblimceq0  34666  knoppndvlem6  34676  bj-bary1lem1  35461  sin2h  35746  itg2addnclem  35807  itg2addnclem3  35809  areacirclem4  35847  ssbnd  35925  lcmineqlem10  40026  lcmineqlem11  40027  lcmineqlem18  40034  lcmineqlem19  40035  sticksstones12a  40093  sticksstones12  40094  metakunt12  40116  mvrrsubd  40283  dffltz  40451  jm2.19lem4  40794  jm2.23  40798  int-eqmvtd  41753  hashnzfzclim  41893  dvradcnv2  41918  binomcxplemnn0  41920  binomcxplemnotnn0  41927  nnsplit  42851  iccshift  43010  iooshift  43014  climinf  43101  limcperiod  43123  0ellimcdiv  43144  cncfshift  43369  cncfperiod  43374  dvdsn1add  43434  dvnmul  43438  dvnprodlem1  43441  itgiccshift  43475  itgperiod  43476  stoweidlem17  43512  wallispilem4  43563  wallispilem5  43564  stirlinglem1  43569  stirlinglem5  43573  stirlinglem6  43574  stirlinglem10  43578  dirkertrigeqlem2  43594  fourierdlem14  43616  fourierdlem19  43621  fourierdlem41  43643  fourierdlem42  43644  fourierdlem48  43649  fourierdlem49  43650  fourierdlem50  43651  fourierdlem64  43665  fourierdlem74  43675  fourierdlem75  43676  fourierdlem81  43682  fourierdlem92  43693  fourierdlem97  43698  fourierdlem103  43704  fourierdlem104  43705  fourierdlem107  43708  etransclem9  43738  nnfoctbdjlem  43947  fldivmod  45816