Theorem npcand 11621

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

Syntax hints:   → wi 4   = wceq 1536   ∈ wcel 2105  (class class class)co 7430  ℂcc 11150   + caddc 11155   − cmin 11489

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-10 2138  ax-11 2154  ax-12 2174  ax-ext 2705  ax-sep 5301  ax-nul 5311  ax-pow 5370  ax-pr 5437  ax-un 7753  ax-resscn 11209  ax-1cn 11210  ax-icn 11211  ax-addcl 11212  ax-addrcl 11213  ax-mulcl 11214  ax-mulrcl 11215  ax-mulcom 11216  ax-addass 11217  ax-mulass 11218  ax-distr 11219  ax-i2m1 11220  ax-1ne0 11221  ax-1rid 11222  ax-rnegex 11223  ax-rrecex 11224  ax-cnre 11225  ax-pre-lttri 11226  ax-pre-lttrn 11227  ax-pre-ltadd 11228

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1539  df-fal 1549  df-ex 1776  df-nf 1780  df-sb 2062  df-mo 2537  df-eu 2566  df-clab 2712  df-cleq 2726  df-clel 2813  df-nfc 2889  df-ne 2938  df-nel 3044  df-ral 3059  df-rex 3068  df-reu 3378  df-rab 3433  df-v 3479  df-sbc 3791  df-csb 3908  df-dif 3965  df-un 3967  df-in 3969  df-ss 3979  df-nul 4339  df-if 4531  df-pw 4606  df-sn 4631  df-pr 4633  df-op 4637  df-uni 4912  df-br 5148  df-opab 5210  df-mpt 5231  df-id 5582  df-po 5596  df-so 5597  df-xp 5694  df-rel 5695  df-cnv 5696  df-co 5697  df-dm 5698  df-rn 5699  df-res 5700  df-ima 5701  df-iota 6515  df-fun 6564  df-fn 6565  df-f 6566  df-f1 6567  df-fo 6568  df-f1o 6569  df-fv 6570  df-riota 7387  df-ov 7433  df-oprab 7434  df-mpo 7435  df-er 8743  df-en 8984  df-dom 8985  df-sdom 8986  df-pnf 11294  df-mnf 11295  df-ltxr 11297  df-sub 11491

This theorem is referenced by:  addlsub  11676  npcan1  11685  ltsubadd  11730  lesubadd  11732  lesub1  11754  lincmb01cmp  13531  expaddzlem  14142  bcpasc  14356  bcn2m1  14359  cshwidxmod  14837  repswcshw  14846  swrds2m  14976  shftuz  15104  o1dif  15662  arisum2  15893  ntrivcvg  15929  ntrivcvgtail  15932  prodrblem  15961  fprodser  15981  fprodm1  15999  risefacval2  16042  fallfacval2  16043  fallfacfwd  16068  binomfallfaclem2  16072  sin01bnd  16217  moddvds  16297  dvdsexp  16361  bitscmp  16471  hashdvds  16808  vdwlem5  17018  vdwlem6  17019  vdwlem8  17021  srgbinomlem4  20246  freshmansdream  21610  psdmul  22187  uniioombllem3  25633  i1faddlem  25741  itg1addlem4  25747  itg1addlem4OLD  25748  dvcnp2  25969  dvcnp2OLD  25970  ftc1lem4  26094  dgrcolem2  26328  plydivlem4  26352  aaliou3lem8  26401  dvtaylp  26426  dvntaylp0  26428  taylthlem1  26429  efif1olem4  26601  tanarg  26675  quart1  26913  dmgmaddnn0  27084  lgamgulm2  27093  gamfac  27124  basellem9  27146  chtublem  27269  logexprlim  27283  dchrptlem1  27322  lgsquadlem1  27438  mudivsum  27588  logsqvma  27600  log2sumbnd  27602  selberglem2  27604  pntrlog2bndlem5  27639  pntlem3  27667  ostth2lem2  27692  brbtwn2  28934  cusgrsize2inds  29485  clwlkclwwlklem2  30028  clwwisshclwws  30043  clwwlkel  30074  clwwlkf  30075  clwwlknonex2lem1  30135  2clwwlk2clwwlk  30378  numclwwlk2  30409  fzspl  32797  fzsplit3  32801  bcm1n  32802  wrdt2ind  32922  swrdrn3  32924  omndmul3  33072  psgnfzto1stlem  33102  cycpmco2lem5  33132  cycpmco2lem6  33133  ballotlemfc0  34473  ballotlemfcc  34474  signstfvn  34562  reprsuc  34608  breprexplemc  34625  lpadlen2  34674  revwlk  35108  bcm1nt  35716  itg2addnclem  37657  ftc1cnnclem  37677  ftc1anc  37687  caushft  37747  fzsplitnd  41963  lcmfunnnd  41993  lcmineqlem4  42013  lcmineqlem23  42032  intlewftc  42042  dvle2  42053  primrootsunit1  42078  aks6d1c5lem3  42118  aks6d1c5lem2  42119  sticksstones10  42136  sticksstones12a  42138  sticksstones16  42143  unitscyglem5  42180  metakunt8  42193  nicomachus  42324  fltnltalem  42648  pellexlem6  42821  rmspecfund  42896  rmyluc  42925  jm2.18  42976  jm2.25  42987  hbtlem4  43114  bccm1k  44337  binomcxplemwb  44343  binomcxplemnotnn0  44351  oddfl  45227  zltlesub  45235  fzisoeu  45250  fperiodmul  45254  fzdifsuc2  45260  iccshift  45470  iooshift  45474  fmul01lt1lem2  45540  limcperiod  45583  sumnnodd  45585  cncfperiod  45834  fperdvper  45874  dvbdfbdioolem2  45884  dvnmul  45898  itgsinexp  45910  itgperiod  45936  stoweidlem11  45966  stoweidlem14  45969  stoweidlem26  45981  stoweidlem34  45989  wallispilem5  46024  stirlinglem5  46033  stirlinglem11  46039  stirlinglem12  46040  dirkercncflem1  46058  fourierdlem11  46073  fourierdlem15  46077  fourierdlem26  46088  fourierdlem41  46103  fourierdlem42  46104  fourierdlem48  46109  fourierdlem49  46110  fourierdlem63  46124  fourierdlem64  46125  fourierdlem65  46126  fourierdlem74  46135  fourierdlem75  46136  fourierdlem79  46140  fourierdlem81  46142  fourierdlem84  46145  fourierdlem88  46149  fourierdlem90  46151  fourierdlem92  46153  fourierdlem95  46156  fourierdlem97  46158  fourierdlem103  46164  fourierdlem104  46165  fourierdlem109  46170  fourierdlem111  46172  fourierswlem  46185  fouriersw  46186  elaa2lem  46188  etransclem23  46212  etransclem24  46213  etransclem28  46217  etransclem38  46227  smfmullem1  46746  fargshiftfo  47366  lighneallem3  47531  nnsum4primeseven  47724  nnsum4primesevenALTV  47725  bgoldbtbndlem4  47732  bgoldbtbnd  47733  gpgedgvtx1  47954  m1modmmod  48370  dignn0flhalflem1  48464  affineid  48553  eenglngeehlnmlem1  48586  itsclquadb  48625