Theorem pncand 11504

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

Syntax hints:   → wi 4   = wceq 1547   ∈ wcel 2119  (class class class)co 7363  ℂcc 11034   + caddc 11039   − cmin 11375

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-10 2152  ax-11 2168  ax-12 2189  ax-ext 2712  ax-sep 5225  ax-nul 5235  ax-pow 5301  ax-pr 5369  ax-un 7685  ax-resscn 11093  ax-1cn 11094  ax-icn 11095  ax-addcl 11096  ax-addrcl 11097  ax-mulcl 11098  ax-mulrcl 11099  ax-mulcom 11100  ax-addass 11101  ax-mulass 11102  ax-distr 11103  ax-i2m1 11104  ax-1ne0 11105  ax-1rid 11106  ax-rnegex 11107  ax-rrecex 11108  ax-cnre 11109  ax-pre-lttri 11110  ax-pre-lttrn 11111  ax-pre-ltadd 11112

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-3or 1093  df-3an 1094  df-tru 1550  df-fal 1560  df-ex 1787  df-nf 1791  df-sb 2074  df-mo 2543  df-eu 2573  df-clab 2719  df-cleq 2732  df-clel 2815  df-nfc 2889  df-ne 2936  df-nel 3040  df-ral 3055  df-rex 3065  df-reu 3346  df-rab 3393  df-v 3434  df-sbc 3731  df-csb 3839  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-nul 4269  df-if 4462  df-pw 4538  df-sn 4563  df-pr 4565  df-op 4569  df-uni 4846  df-br 5080  df-opab 5142  df-mpt 5161  df-id 5520  df-po 5533  df-so 5534  df-xp 5631  df-rel 5632  df-cnv 5633  df-co 5634  df-dm 5635  df-rn 5636  df-res 5637  df-ima 5638  df-iota 6448  df-fun 6494  df-fn 6495  df-f 6496  df-f1 6497  df-fo 6498  df-f1o 6499  df-fv 6500  df-riota 7320  df-ov 7366  df-oprab 7367  df-mpo 7368  df-er 8640  df-en 8891  df-dom 8892  df-sdom 8893  df-pnf 11179  df-mnf 11180  df-ltxr 11182  df-sub 11377

This theorem is referenced by:  mvlraddd  11558  mvlladdd  11559  mvrraddd  11560  addlsub  11564  pnpncand  11569  pncan1  11572  eluzmn  12793  icoshftf1o  13425  xov1plusxeqvd  13449  fzom1ne1  13738  modaddb  13866  zesq  14186  hashdifsnp1  14466  ccatval3  14539  fsump1  15716  fsumrev2  15742  fprodp1  15932  risefacp1  15992  fallfacp1  15993  sadcp1  16422  smupp1  16447  hashdvds  16743  pythagtriplem4  16788  pythagtriplem6  16790  pythagtriplem7  16791  pythagtriplem12  16795  pythagtriplem14  16797  pcqdiv  16826  chnub  18586  chnlt  18587  chnccat  18590  mulgdirlem  19079  psdmplcl  22157  cayhamlem1  22856  pjthlem1  25429  ovolicopnf  25516  i1faddlem  25685  itg1addlem4  25691  itgpowd  26042  taylthlem2  26364  ulmshft  26380  efif1olem2  26532  efif1olem4  26534  logdiflbnd  26983  lgamgulmlem2  27018  lgamcvg2  27043  relgamcl  27050  ftalem2  27062  mulog2sumlem1  27522  mulog2sumlem3  27524  pntrlog2bndlem2  27566  pntrlog2bndlem4  27568  pntrlog2bndlem5  27569  colinearalglem4  29003  axpaschlem  29034  wwlksnred  29985  wwlksnext  29986  wwlksnredwwlkn  29988  wwlksnextproplem2  30003  clwlkclwwlklem2  30095  clwlkclwwlklem3  30096  clwwlkf  30142  wwlksext2clwwlk  30152  eucrct2eupth  30340  numclwwlk2lem1  30471  numclwlk2lem2f  30472  pjhthlem1  31487  fzm1ne1  32887  wrdt2ind  33039  cshwrnid  33047  psgnfzto1stlem  33188  cycpmco2lem4  33217  cycpmco2lem5  33218  cycpmco2lem7  33220  esplyindfv  33767  constraddcl  33953  constrremulcl  33958  madjusmdetlem2  34019  dya2icoseg  34468  fibp1  34592  ballotlemfc0  34684  ballotlemfcc  34685  ballotlemsgt1  34702  ballotlemsel1i  34704  ballotlemsima  34707  ballotlem1ri  34726  signstfvn  34760  reprsuc  34806  bcprod  35973  bccolsum  35974  unblimceq0  36820  knoppndvlem6  36830  bj-bary1lem1  37678  sin2h  37984  itg2addnclem  38045  itg2addnclem3  38047  areacirclem4  38085  ssbnd  38162  lcmineqlem10  42530  lcmineqlem11  42531  lcmineqlem18  42538  lcmineqlem19  42539  sticksstones12a  42649  sticksstones12  42650  aks6d1c6lem3  42664  bcle2d  42671  aks6d1c7lem1  42672  mvrrsubd  42758  fz1sump1  42794  oddnumth  42795  dffltz  43091  jm2.19lem4  43444  jm2.23  43448  int-eqmvtd  44640  hashnzfzclim  44773  dvradcnv2  44798  binomcxplemnn0  44800  binomcxplemnotnn0  44807  nnsplit  45810  iccshift  45970  iooshift  45974  climinf  46058  limcperiod  46080  0ellimcdiv  46099  cncfshift  46324  cncfperiod  46329  dvdsn1add  46389  dvnmul  46393  itgiccshift  46430  itgperiod  46431  stoweidlem17  46467  wallispilem4  46518  wallispilem5  46519  stirlinglem1  46524  stirlinglem5  46528  stirlinglem6  46529  stirlinglem10  46533  dirkertrigeqlem2  46549  fourierdlem14  46571  fourierdlem19  46576  fourierdlem41  46598  fourierdlem42  46599  fourierdlem48  46604  fourierdlem49  46605  fourierdlem50  46606  fourierdlem64  46620  fourierdlem74  46630  fourierdlem75  46631  fourierdlem81  46637  fourierdlem92  46648  fourierdlem97  46653  fourierdlem103  46659  fourierdlem104  46660  fourierdlem107  46663  etransclem9  46693  nnfoctbdjlem  46905  chnerlem2  47335  fldivmod  47814  gpgvtxedg1  48562