Theorem npcand 11561

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

Syntax hints:   → wi 4   = wceq 1563   ∈ wcel 2145  (class class class)co 7400  ℂcc 11086   + caddc 11091   − cmin 11429

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1818  ax-4 1832  ax-5 1933  ax-6 1990  ax-7 2031  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2215  ax-ext 2737  ax-sep 5251  ax-nul 5261  ax-pow 5327  ax-pr 5395  ax-un 7722  ax-resscn 11145  ax-1cn 11146  ax-icn 11147  ax-addcl 11148  ax-addrcl 11149  ax-mulcl 11150  ax-mulrcl 11151  ax-mulcom 11152  ax-addass 11153  ax-mulass 11154  ax-distr 11155  ax-i2m1 11156  ax-1ne0 11157  ax-1rid 11158  ax-rnegex 11159  ax-rrecex 11160  ax-cnre 11161  ax-pre-lttri 11162  ax-pre-lttrn 11163  ax-pre-ltadd 11164

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3or 1102  df-3an 1103  df-tru 1566  df-fal 1576  df-ex 1803  df-nf 1807  df-sb 2094  df-mo 2569  df-eu 2599  df-clab 2744  df-cleq 2757  df-clel 2840  df-nfc 2914  df-ne 2961  df-nel 3065  df-ral 3080  df-rex 3090  df-reu 3371  df-rab 3418  df-v 3459  df-sbc 3748  df-csb 3856  df-dif 3910  df-un 3912  df-in 3914  df-ss 3924  df-nul 4289  df-if 4484  df-pw 4560  df-sn 4586  df-pr 4588  df-op 4592  df-uni 4869  df-br 5106  df-opab 5168  df-mpt 5187  df-id 5547  df-po 5560  df-so 5561  df-xp 5658  df-rel 5659  df-cnv 5660  df-co 5661  df-dm 5662  df-rn 5663  df-res 5664  df-ima 5665  df-iota 6481  df-fun 6527  df-fn 6528  df-f 6529  df-f1 6530  df-fo 6531  df-f1o 6532  df-fv 6533  df-riota 7357  df-ov 7403  df-oprab 7404  df-mpo 7405  df-er 8682  df-en 8932  df-dom 8933  df-sdom 8934  df-pnf 11233  df-mnf 11234  df-ltxr 11236  df-sub 11431

This theorem is referenced by:  addlsub  11618  npcan1  11627  ltsubadd  11672  lesubadd  11674  lesub1  11696  lincmb01cmp  13513  expaddzlem  14132  bcpasc  14348  bcn2m1  14351  cshwidxmod  14830  repswcshw  14839  swrds2m  14968  shftuz  15096  o1dif  15671  arisum2  15905  ntrivcvg  15941  ntrivcvgtail  15944  prodrblem  15973  fprodser  15993  fprodm1  16011  risefacval2  16054  fallfacval2  16055  fallfacfwd  16080  binomfallfaclem2  16084  sin01bnd  16231  moddvds  16311  dvdsexp  16376  bitscmp  16486  hashdvds  16824  vdwlem5  17035  vdwlem6  17036  vdwlem8  17038  chnrev  18673  omndmul3  20195  srgbinomlem4  20302  freshmansdream  21684  psdmul  22289  uniioombllem3  25705  i1faddlem  25813  itg1addlem4  25819  dvcnp2  26040  ftc1lem4  26159  dgrcolem2  26392  plydivlem4  26418  aaliou3lem8  26467  dvtaylp  26491  dvntaylp0  26493  taylthlem1  26494  efif1olem4  26668  tanarg  26742  quart1  26979  dmgmaddnn0  27149  lgamgulm2  27158  gamfac  27189  basellem9  27211  chtublem  27333  logexprlim  27347  dchrptlem1  27386  lgsquadlem1  27502  mudivsum  27652  logsqvma  27664  log2sumbnd  27666  selberglem2  27668  pntrlog2bndlem5  27703  pntlem3  27731  ostth2lem2  27756  brbtwn2  29164  cusgrsize2inds  29712  clwlkclwwlklem2  30260  clwwisshclwws  30275  clwwlkel  30306  clwwlkf  30307  clwwlknonex2lem1  30367  2clwwlk2clwwlk  30610  numclwwlk2  30641  fzspl  33046  fzsplit3  33050  bcm1n  33052  oexpled  33093  wrdt2ind  33186  swrdrn3  33188  psgnfzto1stlem  33333  cycpmco2lem5  33363  cycpmco2lem6  33364  esplyfvn  33884  vietalem  33886  ballotlemfc0  34800  ballotlemfcc  34801  signstfvn  34873  reprsuc  34919  breprexplemc  34936  lpadlen2  34988  revwlk  35488  bcm1nt  36100  itg2addnclem  38182  ftc1cnnclem  38202  ftc1anc  38212  caushft  38272  fzsplitnd  42611  lcmfunnnd  42641  lcmineqlem4  42661  lcmineqlem23  42680  intlewftc  42690  dvle2  42701  primrootsunit1  42726  aks6d1c5lem3  42766  aks6d1c5lem2  42767  sticksstones10  42784  sticksstones12a  42786  sticksstones16  42791  unitscyglem5  42828  nicomachus  42933  fltnltalem  43256  pellexlem6  43423  rmspecfund  43498  rmyluc  43526  jm2.18  43577  jm2.25  43588  hbtlem4  43715  bccm1k  44916  binomcxplemwb  44922  binomcxplemnotnn0  44930  oddfl  45855  zltlesub  45862  fzisoeu  45877  fperiodmul  45881  fzdifsuc2  45887  iccshift  46092  iooshift  46096  fmul01lt1lem2  46159  limcperiod  46202  sumnnodd  46204  cncfperiod  46451  fperdvper  46491  dvbdfbdioolem2  46501  dvnmul  46515  itgsinexp  46527  itgperiod  46553  stoweidlem11  46583  stoweidlem14  46586  stoweidlem26  46598  stoweidlem34  46606  wallispilem5  46641  stirlinglem5  46650  stirlinglem11  46656  stirlinglem12  46657  dirkercncflem1  46675  fourierdlem11  46690  fourierdlem15  46694  fourierdlem26  46705  fourierdlem41  46720  fourierdlem42  46721  fourierdlem48  46726  fourierdlem49  46727  fourierdlem63  46741  fourierdlem64  46742  fourierdlem65  46743  fourierdlem74  46752  fourierdlem75  46753  fourierdlem79  46757  fourierdlem81  46759  fourierdlem84  46762  fourierdlem88  46766  fourierdlem90  46768  fourierdlem92  46770  fourierdlem95  46773  fourierdlem97  46775  fourierdlem103  46781  fourierdlem104  46782  fourierdlem109  46787  fourierdlem111  46789  fourierswlem  46802  fouriersw  46803  elaa2lem  46805  etransclem23  46829  etransclem24  46830  etransclem28  46834  etransclem38  46844  smfmullem1  47363  m1modmmod  47956  fargshiftfo  48046  lighneallem3  48214  nnsum4primeseven  48420  nnsum4primesevenALTV  48421  bgoldbtbndlem4  48428  bgoldbtbnd  48429  gpgedgvtx1  48682  dignn0flhalflem1  49246  affineid  49335  eenglngeehlnmlem1  49368  itsclquadb  49407