Theorem npcand 11507

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 11400	. 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:  addlsub  11564  npcan1  11573  ltsubadd  11618  lesubadd  11620  lesub1  11642  lincmb01cmp  13446  expaddzlem  14065  bcpasc  14281  bcn2m1  14284  cshwidxmod  14763  repswcshw  14772  swrds2m  14901  shftuz  15029  o1dif  15590  arisum2  15824  ntrivcvg  15860  ntrivcvgtail  15863  prodrblem  15892  fprodser  15912  fprodm1  15930  risefacval2  15973  fallfacval2  15974  fallfacfwd  15999  binomfallfaclem2  16003  sin01bnd  16150  moddvds  16230  dvdsexp  16295  bitscmp  16405  hashdvds  16743  vdwlem5  16954  vdwlem6  16955  vdwlem8  16957  chnrev  18591  omndmul3  20107  srgbinomlem4  20208  freshmansdream  21556  psdmul  22161  uniioombllem3  25577  i1faddlem  25685  itg1addlem4  25691  dvcnp2  25912  ftc1lem4  26031  dgrcolem2  26264  plydivlem4  26287  aaliou3lem8  26336  dvtaylp  26360  dvntaylp0  26362  taylthlem1  26363  efif1olem4  26534  tanarg  26608  quart1  26845  dmgmaddnn0  27015  lgamgulm2  27024  gamfac  27055  basellem9  27077  chtublem  27199  logexprlim  27213  dchrptlem1  27252  lgsquadlem1  27368  mudivsum  27518  logsqvma  27530  log2sumbnd  27532  selberglem2  27534  pntrlog2bndlem5  27569  pntlem3  27597  ostth2lem2  27622  brbtwn2  28999  cusgrsize2inds  29547  clwlkclwwlklem2  30095  clwwisshclwws  30110  clwwlkel  30141  clwwlkf  30142  clwwlknonex2lem1  30202  2clwwlk2clwwlk  30445  numclwwlk2  30476  fzspl  32888  fzsplit3  32892  bcm1n  32894  oexpled  32946  wrdt2ind  33039  swrdrn3  33041  psgnfzto1stlem  33188  cycpmco2lem5  33218  cycpmco2lem6  33219  esplyfvn  33768  vietalem  33770  ballotlemfc0  34684  ballotlemfcc  34685  signstfvn  34760  reprsuc  34806  breprexplemc  34823  lpadlen2  34872  revwlk  35354  bcm1nt  35966  itg2addnclem  38039  ftc1cnnclem  38059  ftc1anc  38069  caushft  38129  fzsplitnd  42468  lcmfunnnd  42498  lcmineqlem4  42518  lcmineqlem23  42537  intlewftc  42547  dvle2  42558  primrootsunit1  42583  aks6d1c5lem3  42623  aks6d1c5lem2  42624  sticksstones10  42641  sticksstones12a  42643  sticksstones16  42648  unitscyglem5  42685  nicomachus  42790  fltnltalem  43113  pellexlem6  43280  rmspecfund  43355  rmyluc  43383  jm2.18  43434  jm2.25  43445  hbtlem4  43572  bccm1k  44787  binomcxplemwb  44793  binomcxplemnotnn0  44801  oddfl  45727  zltlesub  45734  fzisoeu  45749  fperiodmul  45753  fzdifsuc2  45759  iccshift  45964  iooshift  45968  fmul01lt1lem2  46031  limcperiod  46074  sumnnodd  46076  cncfperiod  46323  fperdvper  46363  dvbdfbdioolem2  46373  dvnmul  46387  itgsinexp  46399  itgperiod  46425  stoweidlem11  46455  stoweidlem14  46458  stoweidlem26  46470  stoweidlem34  46478  wallispilem5  46513  stirlinglem5  46522  stirlinglem11  46528  stirlinglem12  46529  dirkercncflem1  46547  fourierdlem11  46562  fourierdlem15  46566  fourierdlem26  46577  fourierdlem41  46592  fourierdlem42  46593  fourierdlem48  46598  fourierdlem49  46599  fourierdlem63  46613  fourierdlem64  46614  fourierdlem65  46615  fourierdlem74  46624  fourierdlem75  46625  fourierdlem79  46629  fourierdlem81  46631  fourierdlem84  46634  fourierdlem88  46638  fourierdlem90  46640  fourierdlem92  46642  fourierdlem95  46645  fourierdlem97  46647  fourierdlem103  46653  fourierdlem104  46654  fourierdlem109  46659  fourierdlem111  46661  fourierswlem  46674  fouriersw  46675  elaa2lem  46677  etransclem23  46701  etransclem24  46702  etransclem28  46706  etransclem38  46716  smfmullem1  47235  m1modmmod  47828  fargshiftfo  47918  lighneallem3  48086  nnsum4primeseven  48292  nnsum4primesevenALTV  48293  bgoldbtbndlem4  48300  bgoldbtbnd  48301  gpgedgvtx1  48554  dignn0flhalflem1  49107  affineid  49196  eenglngeehlnmlem1  49229  itsclquadb  49268