Theorem npcand 11500

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

Syntax hints:   → wi 4   = wceq 1542   ∈ wcel 2114  (class class class)co 7360  ℂcc 11028   + caddc 11033   − cmin 11368

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 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2709  ax-sep 5242  ax-nul 5252  ax-pow 5311  ax-pr 5378  ax-un 7682  ax-resscn 11087  ax-1cn 11088  ax-icn 11089  ax-addcl 11090  ax-addrcl 11091  ax-mulcl 11092  ax-mulrcl 11093  ax-mulcom 11094  ax-addass 11095  ax-mulass 11096  ax-distr 11097  ax-i2m1 11098  ax-1ne0 11099  ax-1rid 11100  ax-rnegex 11101  ax-rrecex 11102  ax-cnre 11103  ax-pre-lttri 11104  ax-pre-lttrn 11105  ax-pre-ltadd 11106

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2540  df-eu 2570  df-clab 2716  df-cleq 2729  df-clel 2812  df-nfc 2886  df-ne 2934  df-nel 3038  df-ral 3053  df-rex 3062  df-reu 3352  df-rab 3401  df-v 3443  df-sbc 3742  df-csb 3851  df-dif 3905  df-un 3907  df-in 3909  df-ss 3919  df-nul 4287  df-if 4481  df-pw 4557  df-sn 4582  df-pr 4584  df-op 4588  df-uni 4865  df-br 5100  df-opab 5162  df-mpt 5181  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 6449  df-fun 6495  df-fn 6496  df-f 6497  df-f1 6498  df-fo 6499  df-f1o 6500  df-fv 6501  df-riota 7317  df-ov 7363  df-oprab 7364  df-mpo 7365  df-er 8637  df-en 8888  df-dom 8889  df-sdom 8890  df-pnf 11172  df-mnf 11173  df-ltxr 11175  df-sub 11370

This theorem is referenced by:  addlsub  11557  npcan1  11566  ltsubadd  11611  lesubadd  11613  lesub1  11635  lincmb01cmp  13415  expaddzlem  14032  bcpasc  14248  bcn2m1  14251  cshwidxmod  14730  repswcshw  14739  swrds2m  14868  shftuz  14996  o1dif  15557  arisum2  15788  ntrivcvg  15824  ntrivcvgtail  15827  prodrblem  15856  fprodser  15876  fprodm1  15894  risefacval2  15937  fallfacval2  15938  fallfacfwd  15963  binomfallfaclem2  15967  sin01bnd  16114  moddvds  16194  dvdsexp  16259  bitscmp  16369  hashdvds  16706  vdwlem5  16917  vdwlem6  16918  vdwlem8  16920  chnrev  18554  omndmul3  20067  srgbinomlem4  20168  freshmansdream  21533  psdmul  22113  uniioombllem3  25546  i1faddlem  25654  itg1addlem4  25660  dvcnp2  25881  dvcnp2OLD  25882  ftc1lem4  26006  dgrcolem2  26240  plydivlem4  26264  aaliou3lem8  26313  dvtaylp  26338  dvntaylp0  26340  taylthlem1  26341  efif1olem4  26514  tanarg  26588  quart1  26826  dmgmaddnn0  26997  lgamgulm2  27006  gamfac  27037  basellem9  27059  chtublem  27182  logexprlim  27196  dchrptlem1  27235  lgsquadlem1  27351  mudivsum  27501  logsqvma  27513  log2sumbnd  27515  selberglem2  27517  pntrlog2bndlem5  27552  pntlem3  27580  ostth2lem2  27605  brbtwn2  28961  cusgrsize2inds  29510  clwlkclwwlklem2  30058  clwwisshclwws  30073  clwwlkel  30104  clwwlkf  30105  clwwlknonex2lem1  30165  2clwwlk2clwwlk  30408  numclwwlk2  30439  fzspl  32850  fzsplit3  32854  bcm1n  32856  oexpled  32909  wrdt2ind  33016  swrdrn3  33018  psgnfzto1stlem  33163  cycpmco2lem5  33193  cycpmco2lem6  33194  esplyfvn  33714  vietalem  33716  ballotlemfc0  34631  ballotlemfcc  34632  signstfvn  34707  reprsuc  34753  breprexplemc  34770  lpadlen2  34819  revwlk  35300  bcm1nt  35912  itg2addnclem  37843  ftc1cnnclem  37863  ftc1anc  37873  caushft  37933  fzsplitnd  42273  lcmfunnnd  42303  lcmineqlem4  42323  lcmineqlem23  42342  intlewftc  42352  dvle2  42363  primrootsunit1  42388  aks6d1c5lem3  42428  aks6d1c5lem2  42429  sticksstones10  42446  sticksstones12a  42448  sticksstones16  42453  unitscyglem5  42490  nicomachus  42603  fltnltalem  42941  pellexlem6  43112  rmspecfund  43187  rmyluc  43215  jm2.18  43266  jm2.25  43277  hbtlem4  43404  bccm1k  44619  binomcxplemwb  44625  binomcxplemnotnn0  44633  oddfl  45562  zltlesub  45569  fzisoeu  45584  fperiodmul  45588  fzdifsuc2  45594  iccshift  45800  iooshift  45804  fmul01lt1lem2  45867  limcperiod  45910  sumnnodd  45912  cncfperiod  46159  fperdvper  46199  dvbdfbdioolem2  46209  dvnmul  46223  itgsinexp  46235  itgperiod  46261  stoweidlem11  46291  stoweidlem14  46294  stoweidlem26  46306  stoweidlem34  46314  wallispilem5  46349  stirlinglem5  46358  stirlinglem11  46364  stirlinglem12  46365  dirkercncflem1  46383  fourierdlem11  46398  fourierdlem15  46402  fourierdlem26  46413  fourierdlem41  46428  fourierdlem42  46429  fourierdlem48  46434  fourierdlem49  46435  fourierdlem63  46449  fourierdlem64  46450  fourierdlem65  46451  fourierdlem74  46460  fourierdlem75  46461  fourierdlem79  46465  fourierdlem81  46467  fourierdlem84  46470  fourierdlem88  46474  fourierdlem90  46476  fourierdlem92  46478  fourierdlem95  46481  fourierdlem97  46483  fourierdlem103  46489  fourierdlem104  46490  fourierdlem109  46495  fourierdlem111  46497  fourierswlem  46510  fouriersw  46511  elaa2lem  46513  etransclem23  46537  etransclem24  46538  etransclem28  46542  etransclem38  46552  smfmullem1  47071  m1modmmod  47640  fargshiftfo  47724  lighneallem3  47889  nnsum4primeseven  48082  nnsum4primesevenALTV  48083  bgoldbtbndlem4  48090  bgoldbtbnd  48091  gpgedgvtx1  48344  dignn0flhalflem1  48897  affineid  48986  eenglngeehlnmlem1  49019  itsclquadb  49058