Theorem npcand 11386

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

Syntax hints:   → wi 4   = wceq 1539   ∈ wcel 2104  (class class class)co 7307  ℂcc 10919   + caddc 10924   − cmin 11255

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 1911  ax-6 1969  ax-7 2009  ax-8 2106  ax-9 2114  ax-10 2135  ax-11 2152  ax-12 2169  ax-ext 2707  ax-sep 5232  ax-nul 5239  ax-pow 5297  ax-pr 5361  ax-un 7620  ax-resscn 10978  ax-1cn 10979  ax-icn 10980  ax-addcl 10981  ax-addrcl 10982  ax-mulcl 10983  ax-mulrcl 10984  ax-mulcom 10985  ax-addass 10986  ax-mulass 10987  ax-distr 10988  ax-i2m1 10989  ax-1ne0 10990  ax-1rid 10991  ax-rnegex 10992  ax-rrecex 10993  ax-cnre 10994  ax-pre-lttri 10995  ax-pre-lttrn 10996  ax-pre-ltadd 10997

This theorem depends on definitions:  df-bi 206  df-an 398  df-or 846  df-3or 1088  df-3an 1089  df-tru 1542  df-fal 1552  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2538  df-eu 2567  df-clab 2714  df-cleq 2728  df-clel 2814  df-nfc 2887  df-ne 2942  df-nel 3048  df-ral 3063  df-rex 3072  df-reu 3305  df-rab 3306  df-v 3439  df-sbc 3722  df-csb 3838  df-dif 3895  df-un 3897  df-in 3899  df-ss 3909  df-nul 4263  df-if 4466  df-pw 4541  df-sn 4566  df-pr 4568  df-op 4572  df-uni 4845  df-br 5082  df-opab 5144  df-mpt 5165  df-id 5500  df-po 5514  df-so 5515  df-xp 5606  df-rel 5607  df-cnv 5608  df-co 5609  df-dm 5610  df-rn 5611  df-res 5612  df-ima 5613  df-iota 6410  df-fun 6460  df-fn 6461  df-f 6462  df-f1 6463  df-fo 6464  df-f1o 6465  df-fv 6466  df-riota 7264  df-ov 7310  df-oprab 7311  df-mpo 7312  df-er 8529  df-en 8765  df-dom 8766  df-sdom 8767  df-pnf 11061  df-mnf 11062  df-ltxr 11064  df-sub 11257

This theorem is referenced by:  addlsub  11441  npcan1  11450  ltsubadd  11495  lesubadd  11497  lesub1  11519  lincmb01cmp  13277  expaddzlem  13876  bcpasc  14085  bcn2m1  14088  cshwidxmod  14565  repswcshw  14574  swrds2m  14703  shftuz  14829  o1dif  15388  arisum2  15622  ntrivcvg  15658  ntrivcvgtail  15661  prodrblem  15688  fprodser  15708  fprodm1  15726  risefacval2  15769  fallfacval2  15770  fallfacfwd  15795  binomfallfaclem2  15799  sin01bnd  15943  moddvds  16023  dvdsexp  16086  bitscmp  16194  hashdvds  16525  vdwlem5  16735  vdwlem6  16736  vdwlem8  16738  srgbinomlem4  19828  uniioombllem3  24798  i1faddlem  24906  itg1addlem4  24912  itg1addlem4OLD  24913  dvcnp2  25133  ftc1lem4  25252  dgrcolem2  25484  plydivlem4  25505  aaliou3lem8  25554  dvtaylp  25578  dvntaylp0  25580  taylthlem1  25581  efif1olem4  25750  tanarg  25823  quart1  26055  dmgmaddnn0  26225  lgamgulm2  26234  gamfac  26265  basellem9  26287  chtublem  26408  logexprlim  26422  dchrptlem1  26461  lgsquadlem1  26577  mudivsum  26727  logsqvma  26739  log2sumbnd  26741  selberglem2  26743  pntrlog2bndlem5  26778  pntlem3  26806  ostth2lem2  26831  brbtwn2  27322  cusgrsize2inds  27869  clwlkclwwlklem2  28413  clwwisshclwws  28428  clwwlkel  28459  clwwlkf  28460  clwwlknonex2lem1  28520  2clwwlk2clwwlk  28763  numclwwlk2  28794  fzspl  31160  fzsplit3  31164  bcm1n  31165  wrdt2ind  31274  swrdrn3  31276  omndmul3  31388  psgnfzto1stlem  31416  cycpmco2lem5  31446  cycpmco2lem6  31447  freshmansdream  31533  ballotlemfc0  32508  ballotlemfcc  32509  signstfvn  32597  reprsuc  32644  breprexplemc  32661  lpadlen2  32710  revwlk  33135  bcm1nt  33752  itg2addnclem  35876  ftc1cnnclem  35896  ftc1anc  35906  caushft  35967  fzsplitnd  40191  lcmfunnnd  40220  lcmineqlem4  40240  lcmineqlem23  40259  intlewftc  40269  dvle2  40280  sticksstones10  40311  sticksstones12a  40313  sticksstones16  40318  metakunt8  40332  fltnltalem  40694  pellexlem6  40851  rmspecfund  40926  rmyluc  40955  jm2.18  41006  jm2.25  41017  hbtlem4  41147  bccm1k  42173  binomcxplemwb  42179  binomcxplemnotnn0  42187  oddfl  43044  zltlesub  43052  fzisoeu  43067  fperiodmul  43071  fzdifsuc2  43077  iccshift  43285  iooshift  43289  fmul01lt1lem2  43355  limcperiod  43398  sumnnodd  43400  cncfperiod  43649  fperdvper  43689  dvbdfbdioolem2  43699  dvnmul  43713  itgsinexp  43725  itgperiod  43751  stoweidlem11  43781  stoweidlem14  43784  stoweidlem26  43796  stoweidlem34  43804  wallispilem5  43839  stirlinglem5  43848  stirlinglem11  43854  stirlinglem12  43855  dirkercncflem1  43873  fourierdlem11  43888  fourierdlem15  43892  fourierdlem26  43903  fourierdlem41  43918  fourierdlem42  43919  fourierdlem48  43924  fourierdlem49  43925  fourierdlem63  43939  fourierdlem64  43940  fourierdlem65  43941  fourierdlem74  43950  fourierdlem75  43951  fourierdlem79  43955  fourierdlem81  43957  fourierdlem84  43960  fourierdlem88  43964  fourierdlem90  43966  fourierdlem92  43968  fourierdlem95  43971  fourierdlem97  43973  fourierdlem103  43979  fourierdlem104  43980  fourierdlem109  43985  fourierdlem111  43987  fourierswlem  44000  fouriersw  44001  elaa2lem  44003  etransclem23  44027  etransclem24  44028  etransclem28  44032  etransclem38  44042  smfmullem1  44559  fargshiftfo  45138  lighneallem3  45303  nnsum4primeseven  45496  nnsum4primesevenALTV  45497  bgoldbtbndlem4  45504  bgoldbtbnd  45505  m1modmmod  46111  dignn0flhalflem1  46205  affineid  46294  eenglngeehlnmlem1  46327  itsclquadb  46366