Theorem npcand 11508

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

Syntax hints:   → wi 4   = wceq 1542   ∈ wcel 2114  (class class class)co 7368  ℂcc 11036   + caddc 11041   − cmin 11376

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 5243  ax-nul 5253  ax-pow 5312  ax-pr 5379  ax-un 7690  ax-resscn 11095  ax-1cn 11096  ax-icn 11097  ax-addcl 11098  ax-addrcl 11099  ax-mulcl 11100  ax-mulrcl 11101  ax-mulcom 11102  ax-addass 11103  ax-mulass 11104  ax-distr 11105  ax-i2m1 11106  ax-1ne0 11107  ax-1rid 11108  ax-rnegex 11109  ax-rrecex 11110  ax-cnre 11111  ax-pre-lttri 11112  ax-pre-lttrn 11113  ax-pre-ltadd 11114

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 3063  df-reu 3353  df-rab 3402  df-v 3444  df-sbc 3743  df-csb 3852  df-dif 3906  df-un 3908  df-in 3910  df-ss 3920  df-nul 4288  df-if 4482  df-pw 4558  df-sn 4583  df-pr 4585  df-op 4589  df-uni 4866  df-br 5101  df-opab 5163  df-mpt 5182  df-id 5527  df-po 5540  df-so 5541  df-xp 5638  df-rel 5639  df-cnv 5640  df-co 5641  df-dm 5642  df-rn 5643  df-res 5644  df-ima 5645  df-iota 6456  df-fun 6502  df-fn 6503  df-f 6504  df-f1 6505  df-fo 6506  df-f1o 6507  df-fv 6508  df-riota 7325  df-ov 7371  df-oprab 7372  df-mpo 7373  df-er 8645  df-en 8896  df-dom 8897  df-sdom 8898  df-pnf 11180  df-mnf 11181  df-ltxr 11183  df-sub 11378

This theorem is referenced by:  addlsub  11565  npcan1  11574  ltsubadd  11619  lesubadd  11621  lesub1  11643  lincmb01cmp  13423  expaddzlem  14040  bcpasc  14256  bcn2m1  14259  cshwidxmod  14738  repswcshw  14747  swrds2m  14876  shftuz  15004  o1dif  15565  arisum2  15796  ntrivcvg  15832  ntrivcvgtail  15835  prodrblem  15864  fprodser  15884  fprodm1  15902  risefacval2  15945  fallfacval2  15946  fallfacfwd  15971  binomfallfaclem2  15975  sin01bnd  16122  moddvds  16202  dvdsexp  16267  bitscmp  16377  hashdvds  16714  vdwlem5  16925  vdwlem6  16926  vdwlem8  16928  chnrev  18562  omndmul3  20075  srgbinomlem4  20176  freshmansdream  21541  psdmul  22121  uniioombllem3  25554  i1faddlem  25662  itg1addlem4  25668  dvcnp2  25889  dvcnp2OLD  25890  ftc1lem4  26014  dgrcolem2  26248  plydivlem4  26272  aaliou3lem8  26321  dvtaylp  26346  dvntaylp0  26348  taylthlem1  26349  efif1olem4  26522  tanarg  26596  quart1  26834  dmgmaddnn0  27005  lgamgulm2  27014  gamfac  27045  basellem9  27067  chtublem  27190  logexprlim  27204  dchrptlem1  27243  lgsquadlem1  27359  mudivsum  27509  logsqvma  27521  log2sumbnd  27523  selberglem2  27525  pntrlog2bndlem5  27560  pntlem3  27588  ostth2lem2  27613  brbtwn2  28990  cusgrsize2inds  29539  clwlkclwwlklem2  30087  clwwisshclwws  30102  clwwlkel  30133  clwwlkf  30134  clwwlknonex2lem1  30194  2clwwlk2clwwlk  30437  numclwwlk2  30468  fzspl  32879  fzsplit3  32883  bcm1n  32885  oexpled  32938  wrdt2ind  33045  swrdrn3  33047  psgnfzto1stlem  33193  cycpmco2lem5  33223  cycpmco2lem6  33224  esplyfvn  33753  vietalem  33755  ballotlemfc0  34670  ballotlemfcc  34671  signstfvn  34746  reprsuc  34792  breprexplemc  34809  lpadlen2  34858  revwlk  35338  bcm1nt  35950  itg2addnclem  37911  ftc1cnnclem  37931  ftc1anc  37941  caushft  38001  fzsplitnd  42341  lcmfunnnd  42371  lcmineqlem4  42391  lcmineqlem23  42410  intlewftc  42420  dvle2  42431  primrootsunit1  42456  aks6d1c5lem3  42496  aks6d1c5lem2  42497  sticksstones10  42514  sticksstones12a  42516  sticksstones16  42521  unitscyglem5  42558  nicomachus  42671  fltnltalem  43009  pellexlem6  43180  rmspecfund  43255  rmyluc  43283  jm2.18  43334  jm2.25  43345  hbtlem4  43472  bccm1k  44687  binomcxplemwb  44693  binomcxplemnotnn0  44701  oddfl  45629  zltlesub  45636  fzisoeu  45651  fperiodmul  45655  fzdifsuc2  45661  iccshift  45867  iooshift  45871  fmul01lt1lem2  45934  limcperiod  45977  sumnnodd  45979  cncfperiod  46226  fperdvper  46266  dvbdfbdioolem2  46276  dvnmul  46290  itgsinexp  46302  itgperiod  46328  stoweidlem11  46358  stoweidlem14  46361  stoweidlem26  46373  stoweidlem34  46381  wallispilem5  46416  stirlinglem5  46425  stirlinglem11  46431  stirlinglem12  46432  dirkercncflem1  46450  fourierdlem11  46465  fourierdlem15  46469  fourierdlem26  46480  fourierdlem41  46495  fourierdlem42  46496  fourierdlem48  46501  fourierdlem49  46502  fourierdlem63  46516  fourierdlem64  46517  fourierdlem65  46518  fourierdlem74  46527  fourierdlem75  46528  fourierdlem79  46532  fourierdlem81  46534  fourierdlem84  46537  fourierdlem88  46541  fourierdlem90  46543  fourierdlem92  46545  fourierdlem95  46548  fourierdlem97  46550  fourierdlem103  46556  fourierdlem104  46557  fourierdlem109  46562  fourierdlem111  46564  fourierswlem  46577  fouriersw  46578  elaa2lem  46580  etransclem23  46604  etransclem24  46605  etransclem28  46609  etransclem38  46619  smfmullem1  47138  m1modmmod  47707  fargshiftfo  47791  lighneallem3  47956  nnsum4primeseven  48149  nnsum4primesevenALTV  48150  bgoldbtbndlem4  48157  bgoldbtbnd  48158  gpgedgvtx1  48411  dignn0flhalflem1  48964  affineid  49053  eenglngeehlnmlem1  49086  itsclquadb  49125