Theorem npcand 10990

Description: Cancellation law for subtraction. (Contributed by Mario Carneiro, 27-May-2016.)

Hypotheses

Ref	Expression
negidd.1	⊢ (𝜑 → 𝐴 ∈ ℂ)
pncand.2	⊢ (𝜑 → 𝐵 ∈ ℂ)

Assertion

Ref	Expression
npcand	⊢ (𝜑 → ((𝐴 − 𝐵) + 𝐵) = 𝐴)

Proof of Theorem npcand

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

Syntax hints:   → wi 4   = wceq 1538   ∈ wcel 2111  (class class class)co 7135  ℂcc 10524   + caddc 10529   − cmin 10859

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2158  ax-12 2175  ax-ext 2770  ax-sep 5167  ax-nul 5174  ax-pow 5231  ax-pr 5295  ax-un 7441  ax-resscn 10583  ax-1cn 10584  ax-icn 10585  ax-addcl 10586  ax-addrcl 10587  ax-mulcl 10588  ax-mulrcl 10589  ax-mulcom 10590  ax-addass 10591  ax-mulass 10592  ax-distr 10593  ax-i2m1 10594  ax-1ne0 10595  ax-1rid 10596  ax-rnegex 10597  ax-rrecex 10598  ax-cnre 10599  ax-pre-lttri 10600  ax-pre-lttrn 10601  ax-pre-ltadd 10602

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3or 1085  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-mo 2598  df-eu 2629  df-clab 2777  df-cleq 2791  df-clel 2870  df-nfc 2938  df-ne 2988  df-nel 3092  df-ral 3111  df-rex 3112  df-reu 3113  df-rab 3115  df-v 3443  df-sbc 3721  df-csb 3829  df-dif 3884  df-un 3886  df-in 3888  df-ss 3898  df-nul 4244  df-if 4426  df-pw 4499  df-sn 4526  df-pr 4528  df-op 4532  df-uni 4801  df-br 5031  df-opab 5093  df-mpt 5111  df-id 5425  df-po 5438  df-so 5439  df-xp 5525  df-rel 5526  df-cnv 5527  df-co 5528  df-dm 5529  df-rn 5530  df-res 5531  df-ima 5532  df-iota 6283  df-fun 6326  df-fn 6327  df-f 6328  df-f1 6329  df-fo 6330  df-f1o 6331  df-fv 6332  df-riota 7093  df-ov 7138  df-oprab 7139  df-mpo 7140  df-er 8272  df-en 8493  df-dom 8494  df-sdom 8495  df-pnf 10666  df-mnf 10667  df-ltxr 10669  df-sub 10861

This theorem is referenced by:  addlsub  11045  npcan1  11054  ltsubadd  11099  lesubadd  11101  lesub1  11123  lincmb01cmp  12873  expaddzlem  13468  bcpasc  13677  bcn2m1  13680  cshwidxmod  14156  repswcshw  14165  swrds2m  14294  shftuz  14420  o1dif  14978  arisum2  15208  ntrivcvg  15245  ntrivcvgtail  15248  prodrblem  15275  fprodser  15295  fprodm1  15313  risefacval2  15356  fallfacval2  15357  fallfacfwd  15382  binomfallfaclem2  15386  sin01bnd  15530  moddvds  15610  dvdsexp  15669  bitscmp  15777  hashdvds  16102  vdwlem5  16311  vdwlem6  16312  vdwlem8  16314  srgbinomlem4  19286  uniioombllem3  24189  i1faddlem  24297  itg1addlem4  24303  dvcnp2  24523  ftc1lem4  24642  dgrcolem2  24871  plydivlem4  24892  aaliou3lem8  24941  dvtaylp  24965  dvntaylp0  24967  taylthlem1  24968  efif1olem4  25137  tanarg  25210  quart1  25442  dmgmaddnn0  25612  lgamgulm2  25621  gamfac  25652  basellem9  25674  chtublem  25795  logexprlim  25809  dchrptlem1  25848  lgsquadlem1  25964  mudivsum  26114  logsqvma  26126  log2sumbnd  26128  selberglem2  26130  pntrlog2bndlem5  26165  pntlem3  26193  ostth2lem2  26218  brbtwn2  26699  cusgrsize2inds  27243  clwlkclwwlklem2  27785  clwwisshclwws  27800  clwwlkel  27831  clwwlkf  27832  clwwlknonex2lem1  27892  2clwwlk2clwwlk  28135  numclwwlk2  28166  fzspl  30539  fzsplit3  30543  bcm1n  30544  wrdt2ind  30653  swrdrn3  30655  omndmul3  30764  psgnfzto1stlem  30792  cycpmco2lem5  30822  cycpmco2lem6  30823  freshmansdream  30909  ballotlemfc0  31860  ballotlemfcc  31861  signstfvn  31949  reprsuc  31996  breprexplemc  32013  lpadlen2  32062  revwlk  32484  bcm1nt  33082  itg2addnclem  35108  ftc1cnnclem  35128  ftc1anc  35138  caushft  35199  fzsplitnd  39270  lcmfunnnd  39300  lcmineqlem4  39320  lcmineqlem23  39339  intlewftc  39344  metakunt8  39357  fltnltalem  39618  pellexlem6  39775  rmspecfund  39850  rmyluc  39878  jm2.18  39929  jm2.25  39940  hbtlem4  40070  bccm1k  41046  binomcxplemwb  41052  binomcxplemnotnn0  41060  oddfl  41908  zltlesub  41916  fzisoeu  41932  fperiodmul  41936  fzdifsuc2  41942  iccshift  42155  iooshift  42159  fmul01lt1lem2  42227  limcperiod  42270  sumnnodd  42272  cncfperiod  42521  fperdvper  42561  dvbdfbdioolem2  42571  dvnmul  42585  itgsinexp  42597  itgperiod  42623  stoweidlem11  42653  stoweidlem14  42656  stoweidlem26  42668  stoweidlem34  42676  wallispilem5  42711  stirlinglem5  42720  stirlinglem11  42726  stirlinglem12  42727  dirkercncflem1  42745  fourierdlem11  42760  fourierdlem15  42764  fourierdlem26  42775  fourierdlem41  42790  fourierdlem42  42791  fourierdlem48  42796  fourierdlem49  42797  fourierdlem63  42811  fourierdlem64  42812  fourierdlem65  42813  fourierdlem74  42822  fourierdlem75  42823  fourierdlem79  42827  fourierdlem81  42829  fourierdlem84  42832  fourierdlem88  42836  fourierdlem90  42838  fourierdlem92  42840  fourierdlem95  42843  fourierdlem97  42845  fourierdlem103  42851  fourierdlem104  42852  fourierdlem109  42857  fourierdlem111  42859  fourierswlem  42872  fouriersw  42873  elaa2lem  42875  etransclem23  42899  etransclem24  42900  etransclem28  42904  etransclem38  42914  smfmullem1  43423  fargshiftfo  43959  lighneallem3  44125  nnsum4primeseven  44318  nnsum4primesevenALTV  44319  bgoldbtbndlem4  44326  bgoldbtbnd  44327  m1modmmod  44935  dignn0flhalflem1  45029  affineid  45118  eenglngeehlnmlem1  45151  itsclquadb  45190