Theorem npcand 11479

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

Syntax hints:   → wi 4   = wceq 1540   ∈ wcel 2109  (class class class)co 7349  ℂcc 11007   + caddc 11012   − cmin 11347

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2701  ax-sep 5235  ax-nul 5245  ax-pow 5304  ax-pr 5371  ax-un 7671  ax-resscn 11066  ax-1cn 11067  ax-icn 11068  ax-addcl 11069  ax-addrcl 11070  ax-mulcl 11071  ax-mulrcl 11072  ax-mulcom 11073  ax-addass 11074  ax-mulass 11075  ax-distr 11076  ax-i2m1 11077  ax-1ne0 11078  ax-1rid 11079  ax-rnegex 11080  ax-rrecex 11081  ax-cnre 11082  ax-pre-lttri 11083  ax-pre-lttrn 11084  ax-pre-ltadd 11085

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2533  df-eu 2562  df-clab 2708  df-cleq 2721  df-clel 2803  df-nfc 2878  df-ne 2926  df-nel 3030  df-ral 3045  df-rex 3054  df-reu 3344  df-rab 3395  df-v 3438  df-sbc 3743  df-csb 3852  df-dif 3906  df-un 3908  df-in 3910  df-ss 3920  df-nul 4285  df-if 4477  df-pw 4553  df-sn 4578  df-pr 4580  df-op 4584  df-uni 4859  df-br 5093  df-opab 5155  df-mpt 5174  df-id 5514  df-po 5527  df-so 5528  df-xp 5625  df-rel 5626  df-cnv 5627  df-co 5628  df-dm 5629  df-rn 5630  df-res 5631  df-ima 5632  df-iota 6438  df-fun 6484  df-fn 6485  df-f 6486  df-f1 6487  df-fo 6488  df-f1o 6489  df-fv 6490  df-riota 7306  df-ov 7352  df-oprab 7353  df-mpo 7354  df-er 8625  df-en 8873  df-dom 8874  df-sdom 8875  df-pnf 11151  df-mnf 11152  df-ltxr 11154  df-sub 11349

This theorem is referenced by:  addlsub  11536  npcan1  11545  ltsubadd  11590  lesubadd  11592  lesub1  11614  lincmb01cmp  13398  expaddzlem  14012  bcpasc  14228  bcn2m1  14231  cshwidxmod  14709  repswcshw  14718  swrds2m  14848  shftuz  14976  o1dif  15537  arisum2  15768  ntrivcvg  15804  ntrivcvgtail  15807  prodrblem  15836  fprodser  15856  fprodm1  15874  risefacval2  15917  fallfacval2  15918  fallfacfwd  15943  binomfallfaclem2  15947  sin01bnd  16094  moddvds  16174  dvdsexp  16239  bitscmp  16349  hashdvds  16686  vdwlem5  16897  vdwlem6  16898  vdwlem8  16900  omndmul3  20013  srgbinomlem4  20114  freshmansdream  21481  psdmul  22051  uniioombllem3  25484  i1faddlem  25592  itg1addlem4  25598  dvcnp2  25819  dvcnp2OLD  25820  ftc1lem4  25944  dgrcolem2  26178  plydivlem4  26202  aaliou3lem8  26251  dvtaylp  26276  dvntaylp0  26278  taylthlem1  26279  efif1olem4  26452  tanarg  26526  quart1  26764  dmgmaddnn0  26935  lgamgulm2  26944  gamfac  26975  basellem9  26997  chtublem  27120  logexprlim  27134  dchrptlem1  27173  lgsquadlem1  27289  mudivsum  27439  logsqvma  27451  log2sumbnd  27453  selberglem2  27455  pntrlog2bndlem5  27490  pntlem3  27518  ostth2lem2  27543  brbtwn2  28850  cusgrsize2inds  29399  clwlkclwwlklem2  29944  clwwisshclwws  29959  clwwlkel  29990  clwwlkf  29991  clwwlknonex2lem1  30051  2clwwlk2clwwlk  30294  numclwwlk2  30325  fzspl  32732  fzsplit3  32736  bcm1n  32738  oexpled  32792  wrdt2ind  32895  swrdrn3  32897  psgnfzto1stlem  33042  cycpmco2lem5  33072  cycpmco2lem6  33073  ballotlemfc0  34461  ballotlemfcc  34462  signstfvn  34537  reprsuc  34583  breprexplemc  34600  lpadlen2  34649  revwlk  35102  bcm1nt  35714  itg2addnclem  37655  ftc1cnnclem  37675  ftc1anc  37685  caushft  37745  fzsplitnd  41959  lcmfunnnd  41989  lcmineqlem4  42009  lcmineqlem23  42028  intlewftc  42038  dvle2  42049  primrootsunit1  42074  aks6d1c5lem3  42114  aks6d1c5lem2  42115  sticksstones10  42132  sticksstones12a  42134  sticksstones16  42139  unitscyglem5  42176  nicomachus  42289  fltnltalem  42639  pellexlem6  42811  rmspecfund  42886  rmyluc  42914  jm2.18  42965  jm2.25  42976  hbtlem4  43103  bccm1k  44319  binomcxplemwb  44325  binomcxplemnotnn0  44333  oddfl  45264  zltlesub  45271  fzisoeu  45286  fperiodmul  45290  fzdifsuc2  45296  iccshift  45503  iooshift  45507  fmul01lt1lem2  45570  limcperiod  45613  sumnnodd  45615  cncfperiod  45864  fperdvper  45904  dvbdfbdioolem2  45914  dvnmul  45928  itgsinexp  45940  itgperiod  45966  stoweidlem11  45996  stoweidlem14  45999  stoweidlem26  46011  stoweidlem34  46019  wallispilem5  46054  stirlinglem5  46063  stirlinglem11  46069  stirlinglem12  46070  dirkercncflem1  46088  fourierdlem11  46103  fourierdlem15  46107  fourierdlem26  46118  fourierdlem41  46133  fourierdlem42  46134  fourierdlem48  46139  fourierdlem49  46140  fourierdlem63  46154  fourierdlem64  46155  fourierdlem65  46156  fourierdlem74  46165  fourierdlem75  46166  fourierdlem79  46170  fourierdlem81  46172  fourierdlem84  46175  fourierdlem88  46179  fourierdlem90  46181  fourierdlem92  46183  fourierdlem95  46186  fourierdlem97  46188  fourierdlem103  46194  fourierdlem104  46195  fourierdlem109  46200  fourierdlem111  46202  fourierswlem  46215  fouriersw  46216  elaa2lem  46218  etransclem23  46242  etransclem24  46243  etransclem28  46247  etransclem38  46257  smfmullem1  46776  m1modmmod  47346  fargshiftfo  47430  lighneallem3  47595  nnsum4primeseven  47788  nnsum4primesevenALTV  47789  bgoldbtbndlem4  47796  bgoldbtbnd  47797  gpgedgvtx1  48050  dignn0flhalflem1  48604  affineid  48693  eenglngeehlnmlem1  48726  itsclquadb  48765