Theorem pncand 11600

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

Syntax hints:   → wi 4   = wceq 1540   ∈ wcel 2109  (class class class)co 7410  ℂcc 11132   + caddc 11137   − cmin 11471

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 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2708  ax-sep 5271  ax-nul 5281  ax-pow 5340  ax-pr 5407  ax-un 7734  ax-resscn 11191  ax-1cn 11192  ax-icn 11193  ax-addcl 11194  ax-addrcl 11195  ax-mulcl 11196  ax-mulrcl 11197  ax-mulcom 11198  ax-addass 11199  ax-mulass 11200  ax-distr 11201  ax-i2m1 11202  ax-1ne0 11203  ax-1rid 11204  ax-rnegex 11205  ax-rrecex 11206  ax-cnre 11207  ax-pre-lttri 11208  ax-pre-lttrn 11209  ax-pre-ltadd 11210

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2540  df-eu 2569  df-clab 2715  df-cleq 2728  df-clel 2810  df-nfc 2886  df-ne 2934  df-nel 3038  df-ral 3053  df-rex 3062  df-reu 3365  df-rab 3421  df-v 3466  df-sbc 3771  df-csb 3880  df-dif 3934  df-un 3936  df-in 3938  df-ss 3948  df-nul 4314  df-if 4506  df-pw 4582  df-sn 4607  df-pr 4609  df-op 4613  df-uni 4889  df-br 5125  df-opab 5187  df-mpt 5207  df-id 5553  df-po 5566  df-so 5567  df-xp 5665  df-rel 5666  df-cnv 5667  df-co 5668  df-dm 5669  df-rn 5670  df-res 5671  df-ima 5672  df-iota 6489  df-fun 6538  df-fn 6539  df-f 6540  df-f1 6541  df-fo 6542  df-f1o 6543  df-fv 6544  df-riota 7367  df-ov 7413  df-oprab 7414  df-mpo 7415  df-er 8724  df-en 8965  df-dom 8966  df-sdom 8967  df-pnf 11276  df-mnf 11277  df-ltxr 11279  df-sub 11473

This theorem is referenced by:  mvlraddd  11652  mvlladdd  11653  mvrraddd  11654  addlsub  11658  pnpncand  11663  pncan1  11666  eluzmn  12864  icoshftf1o  13496  xov1plusxeqvd  13520  zesq  14249  hashdifsnp1  14529  ccatval3  14602  fsump1  15777  fsumrev2  15803  fprodp1  15990  risefacp1  16050  fallfacp1  16051  sadcp1  16479  smupp1  16504  hashdvds  16799  pythagtriplem4  16844  pythagtriplem6  16846  pythagtriplem7  16847  pythagtriplem12  16851  pythagtriplem14  16853  pcqdiv  16882  mulgdirlem  19093  psdmplcl  22105  cayhamlem1  22809  pjthlem1  25394  ovolicopnf  25482  i1faddlem  25651  itg1addlem4  25657  itgpowd  26014  taylthlem2  26339  taylthlem2OLD  26340  ulmshft  26356  efif1olem2  26509  efif1olem4  26511  logdiflbnd  26962  lgamgulmlem2  26997  lgamcvg2  27022  relgamcl  27029  ftalem2  27041  mulog2sumlem1  27502  mulog2sumlem3  27504  pntrlog2bndlem2  27546  pntrlog2bndlem4  27548  pntrlog2bndlem5  27549  colinearalglem4  28893  axpaschlem  28924  wwlksnred  29879  wwlksnext  29880  wwlksnredwwlkn  29882  wwlksnextproplem2  29897  clwlkclwwlklem2  29986  clwlkclwwlklem3  29987  clwwlkf  30033  wwlksext2clwwlk  30043  eucrct2eupth  30231  numclwwlk2lem1  30362  numclwlk2lem2f  30363  pjhthlem1  31377  fzm1ne1  32770  fzom1ne1  32783  wrdt2ind  32934  cshwrnid  32942  chnub  32997  chnlt  32998  psgnfzto1stlem  33116  cycpmco2lem4  33145  cycpmco2lem5  33146  cycpmco2lem7  33148  constraddcl  33801  constrremulcl  33806  madjusmdetlem2  33864  dya2icoseg  34314  fibp1  34438  ballotlemfc0  34530  ballotlemfcc  34531  ballotlemsgt1  34548  ballotlemsel1i  34550  ballotlemsima  34553  ballotlem1ri  34572  signstfvn  34606  reprsuc  34652  bcprod  35760  bccolsum  35761  unblimceq0  36530  knoppndvlem6  36540  bj-bary1lem1  37334  sin2h  37639  itg2addnclem  37700  itg2addnclem3  37702  areacirclem4  37740  ssbnd  37817  lcmineqlem10  42056  lcmineqlem11  42057  lcmineqlem18  42064  lcmineqlem19  42065  sticksstones12a  42175  sticksstones12  42176  aks6d1c6lem3  42190  bcle2d  42197  aks6d1c7lem1  42198  mvrrsubd  42292  fz1sump1  42328  oddnumth  42329  dffltz  42632  jm2.19lem4  42991  jm2.23  42995  int-eqmvtd  44188  hashnzfzclim  44321  dvradcnv2  44346  binomcxplemnn0  44348  binomcxplemnotnn0  44355  nnsplit  45365  iccshift  45527  iooshift  45531  climinf  45615  limcperiod  45637  0ellimcdiv  45658  cncfshift  45883  cncfperiod  45888  dvdsn1add  45948  dvnmul  45952  itgiccshift  45989  itgperiod  45990  stoweidlem17  46026  wallispilem4  46077  wallispilem5  46078  stirlinglem1  46083  stirlinglem5  46087  stirlinglem6  46088  stirlinglem10  46092  dirkertrigeqlem2  46108  fourierdlem14  46130  fourierdlem19  46135  fourierdlem41  46157  fourierdlem42  46158  fourierdlem48  46163  fourierdlem49  46164  fourierdlem50  46165  fourierdlem64  46179  fourierdlem74  46189  fourierdlem75  46190  fourierdlem81  46196  fourierdlem92  46207  fourierdlem97  46212  fourierdlem103  46218  fourierdlem104  46219  fourierdlem107  46222  etransclem9  46252  nnfoctbdjlem  46464  fldivmod  47347  gpgvtxedg1  48048