Theorem npcand 11486

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

Syntax hints:   → wi 4   = wceq 1541   ∈ wcel 2113  (class class class)co 7355  ℂcc 11014   + caddc 11019   − cmin 11354

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-10 2146  ax-11 2162  ax-12 2182  ax-ext 2705  ax-sep 5238  ax-nul 5248  ax-pow 5307  ax-pr 5374  ax-un 7677  ax-resscn 11073  ax-1cn 11074  ax-icn 11075  ax-addcl 11076  ax-addrcl 11077  ax-mulcl 11078  ax-mulrcl 11079  ax-mulcom 11080  ax-addass 11081  ax-mulass 11082  ax-distr 11083  ax-i2m1 11084  ax-1ne0 11085  ax-1rid 11086  ax-rnegex 11087  ax-rrecex 11088  ax-cnre 11089  ax-pre-lttri 11090  ax-pre-lttrn 11091  ax-pre-ltadd 11092

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-nf 1785  df-sb 2068  df-mo 2537  df-eu 2566  df-clab 2712  df-cleq 2725  df-clel 2808  df-nfc 2883  df-ne 2931  df-nel 3035  df-ral 3050  df-rex 3059  df-reu 3349  df-rab 3398  df-v 3440  df-sbc 3739  df-csb 3848  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-nul 4285  df-if 4477  df-pw 4553  df-sn 4578  df-pr 4580  df-op 4584  df-uni 4861  df-br 5096  df-opab 5158  df-mpt 5177  df-id 5516  df-po 5529  df-so 5530  df-xp 5627  df-rel 5628  df-cnv 5629  df-co 5630  df-dm 5631  df-rn 5632  df-res 5633  df-ima 5634  df-iota 6445  df-fun 6491  df-fn 6492  df-f 6493  df-f1 6494  df-fo 6495  df-f1o 6496  df-fv 6497  df-riota 7312  df-ov 7358  df-oprab 7359  df-mpo 7360  df-er 8631  df-en 8879  df-dom 8880  df-sdom 8881  df-pnf 11158  df-mnf 11159  df-ltxr 11161  df-sub 11356

This theorem is referenced by:  addlsub  11543  npcan1  11552  ltsubadd  11597  lesubadd  11599  lesub1  11621  lincmb01cmp  13405  expaddzlem  14022  bcpasc  14238  bcn2m1  14241  cshwidxmod  14720  repswcshw  14729  swrds2m  14858  shftuz  14986  o1dif  15547  arisum2  15778  ntrivcvg  15814  ntrivcvgtail  15817  prodrblem  15846  fprodser  15866  fprodm1  15884  risefacval2  15927  fallfacval2  15928  fallfacfwd  15953  binomfallfaclem2  15957  sin01bnd  16104  moddvds  16184  dvdsexp  16249  bitscmp  16359  hashdvds  16696  vdwlem5  16907  vdwlem6  16908  vdwlem8  16910  chnrev  18543  omndmul3  20056  srgbinomlem4  20157  freshmansdream  21521  psdmul  22091  uniioombllem3  25523  i1faddlem  25631  itg1addlem4  25637  dvcnp2  25858  dvcnp2OLD  25859  ftc1lem4  25983  dgrcolem2  26217  plydivlem4  26241  aaliou3lem8  26290  dvtaylp  26315  dvntaylp0  26317  taylthlem1  26318  efif1olem4  26491  tanarg  26565  quart1  26803  dmgmaddnn0  26974  lgamgulm2  26983  gamfac  27014  basellem9  27036  chtublem  27159  logexprlim  27173  dchrptlem1  27212  lgsquadlem1  27328  mudivsum  27478  logsqvma  27490  log2sumbnd  27492  selberglem2  27494  pntrlog2bndlem5  27529  pntlem3  27557  ostth2lem2  27582  brbtwn2  28894  cusgrsize2inds  29443  clwlkclwwlklem2  29991  clwwisshclwws  30006  clwwlkel  30037  clwwlkf  30038  clwwlknonex2lem1  30098  2clwwlk2clwwlk  30341  numclwwlk2  30372  fzspl  32783  fzsplit3  32787  bcm1n  32788  oexpled  32841  wrdt2ind  32945  swrdrn3  32947  psgnfzto1stlem  33080  cycpmco2lem5  33110  cycpmco2lem6  33111  ballotlemfc0  34517  ballotlemfcc  34518  signstfvn  34593  reprsuc  34639  breprexplemc  34656  lpadlen2  34705  revwlk  35180  bcm1nt  35792  itg2addnclem  37721  ftc1cnnclem  37741  ftc1anc  37751  caushft  37811  fzsplitnd  42085  lcmfunnnd  42115  lcmineqlem4  42135  lcmineqlem23  42154  intlewftc  42164  dvle2  42175  primrootsunit1  42200  aks6d1c5lem3  42240  aks6d1c5lem2  42241  sticksstones10  42258  sticksstones12a  42260  sticksstones16  42265  unitscyglem5  42302  nicomachus  42420  fltnltalem  42770  pellexlem6  42941  rmspecfund  43016  rmyluc  43044  jm2.18  43095  jm2.25  43106  hbtlem4  43233  bccm1k  44449  binomcxplemwb  44455  binomcxplemnotnn0  44463  oddfl  45393  zltlesub  45400  fzisoeu  45415  fperiodmul  45419  fzdifsuc2  45425  iccshift  45632  iooshift  45636  fmul01lt1lem2  45699  limcperiod  45742  sumnnodd  45744  cncfperiod  45991  fperdvper  46031  dvbdfbdioolem2  46041  dvnmul  46055  itgsinexp  46067  itgperiod  46093  stoweidlem11  46123  stoweidlem14  46126  stoweidlem26  46138  stoweidlem34  46146  wallispilem5  46181  stirlinglem5  46190  stirlinglem11  46196  stirlinglem12  46197  dirkercncflem1  46215  fourierdlem11  46230  fourierdlem15  46234  fourierdlem26  46245  fourierdlem41  46260  fourierdlem42  46261  fourierdlem48  46266  fourierdlem49  46267  fourierdlem63  46281  fourierdlem64  46282  fourierdlem65  46283  fourierdlem74  46292  fourierdlem75  46293  fourierdlem79  46297  fourierdlem81  46299  fourierdlem84  46302  fourierdlem88  46306  fourierdlem90  46308  fourierdlem92  46310  fourierdlem95  46313  fourierdlem97  46315  fourierdlem103  46321  fourierdlem104  46322  fourierdlem109  46327  fourierdlem111  46329  fourierswlem  46342  fouriersw  46343  elaa2lem  46345  etransclem23  46369  etransclem24  46370  etransclem28  46374  etransclem38  46384  smfmullem1  46903  m1modmmod  47472  fargshiftfo  47556  lighneallem3  47721  nnsum4primeseven  47914  nnsum4primesevenALTV  47915  bgoldbtbndlem4  47922  bgoldbtbnd  47923  gpgedgvtx1  48176  dignn0flhalflem1  48730  affineid  48819  eenglngeehlnmlem1  48852  itsclquadb  48891