Theorem npcand 11572

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

Syntax hints:   → wi 4   = wceq 1568   ∈ wcel 2141  (class class class)co 7410  ℂcc 11097   + caddc 11102   − cmin 11440

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1823  ax-4 1837  ax-5 1938  ax-6 1995  ax-7 2036  ax-8 2143  ax-9 2151  ax-10 2174  ax-11 2190  ax-12 2211  ax-ext 2733  ax-sep 5256  ax-nul 5268  ax-pow 5336  ax-pr 5404  ax-un 7732  ax-resscn 11156  ax-1cn 11157  ax-icn 11158  ax-addcl 11159  ax-addrcl 11160  ax-mulcl 11161  ax-mulrcl 11162  ax-mulcom 11163  ax-addass 11164  ax-mulass 11165  ax-distr 11166  ax-i2m1 11167  ax-1ne0 11168  ax-1rid 11169  ax-rnegex 11170  ax-rrecex 11171  ax-cnre 11172  ax-pre-lttri 11173  ax-pre-lttrn 11174  ax-pre-ltadd 11175

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3or 1102  df-3an 1103  df-tru 1571  df-fal 1581  df-ex 1808  df-nf 1812  df-sb 2095  df-mo 2565  df-eu 2595  df-clab 2740  df-cleq 2753  df-clel 2836  df-nfc 2910  df-ne 2957  df-nel 3063  df-ral 3078  df-rex 3088  df-reu 3368  df-rab 3415  df-v 3455  df-sbc 3744  df-csb 3853  df-dif 3907  df-un 3909  df-in 3911  df-ss 3921  df-nul 4286  df-if 4487  df-pw 4563  df-sn 4589  df-pr 4591  df-op 4595  df-uni 4872  df-br 5109  df-opab 5173  df-mpt 5192  df-id 5556  df-po 5569  df-so 5570  df-xp 5667  df-rel 5668  df-cnv 5669  df-co 5670  df-dm 5671  df-rn 5672  df-res 5673  df-ima 5674  df-iota 6492  df-fun 6538  df-fn 6539  df-f 6540  df-f1 6541  df-fo 6542  df-f1o 6543  df-fv 6544  df-riota 7367  df-ov 7413  df-oprab 7414  df-mpo 7415  df-er 8693  df-en 8943  df-dom 8944  df-sdom 8945  df-pnf 11244  df-mnf 11245  df-ltxr 11247  df-sub 11442

This theorem is referenced by:  addlsub  11629  npcan1  11638  ltsubadd  11683  lesubadd  11685  lesub1  11707  lincmb01cmp  13521  expaddzlem  14141  bcpasc  14357  bcn2m1  14360  cshwidxmod  14840  repswcshw  14849  swrds2m  14978  shftuz  15106  o1dif  15681  arisum2  15915  ntrivcvg  15951  ntrivcvgtail  15954  prodrblem  15983  fprodser  16003  fprodm1  16021  risefacval2  16064  fallfacval2  16065  fallfacfwd  16089  binomfallfaclem2  16093  sin01bnd  16240  moddvds  16320  dvdsexp  16385  bitscmp  16495  hashdvds  16833  vdwlem5  17044  vdwlem6  17045  vdwlem8  17047  chnrev  18682  omndmul3  20203  srgbinomlem4  20310  freshmansdream  21703  psdmul  22308  uniioombllem3  25723  i1faddlem  25831  itg1addlem4  25837  dvcnp2  26058  ftc1lem4  26177  dgrcolem2  26410  plydivlem4  26436  aaliou3lem8  26485  dvtaylp  26509  dvntaylp0  26511  taylthlem1  26512  efif1olem4  26686  tanarg  26760  quart1  26997  dmgmaddnn0  27167  lgamgulm2  27176  gamfac  27207  basellem9  27229  chtublem  27351  logexprlim  27365  dchrptlem1  27404  lgsquadlem1  27520  mudivsum  27670  logsqvma  27682  log2sumbnd  27684  selberglem2  27686  pntrlog2bndlem5  27721  pntlem3  27749  ostth2lem2  27774  brbtwn2  29221  cusgrsize2inds  29769  clwlkclwwlklem2  30317  clwwisshclwws  30332  clwwlkel  30363  clwwlkf  30364  clwwlknonex2lem1  30424  2clwwlk2clwwlk  30667  numclwwlk2  30698  fzspl  33100  fzsplit3  33104  bcm1n  33106  oexpled  33146  wrdt2ind  33239  swrdrn3  33241  psgnfzto1stlem  33386  cycpmco2lem5  33416  cycpmco2lem6  33417  esplyfvn  33933  vietalem  33935  ballotlemfc0  34849  ballotlemfcc  34850  signstfvn  34922  reprsuc  34968  breprexplemc  34985  lpadlen2  35037  revwlk  35583  bcm1nt  36195  itg2addnclem  38288  ftc1cnnclem  38308  ftc1anc  38318  caushft  38378  fzsplitnd  42717  lcmfunnnd  42747  lcmineqlem4  42767  lcmineqlem23  42786  intlewftc  42796  dvle2  42807  primrootsunit1  42832  aks6d1c5lem3  42872  aks6d1c5lem2  42873  sticksstones10  42890  sticksstones12a  42892  sticksstones16  42897  unitscyglem5  42934  nicomachus  43041  fltnltalem  43364  pellexlem6  43531  rmspecfund  43606  rmyluc  43634  jm2.18  43685  jm2.25  43696  hbtlem4  43823  bccm1k  45022  binomcxplemwb  45028  binomcxplemnotnn0  45036  oddfl  45967  zltlesub  45974  fzisoeu  45989  fperiodmul  45993  fzdifsuc2  45999  iccshift  46204  iooshift  46208  fmul01lt1lem2  46271  limcperiod  46314  sumnnodd  46316  cncfperiod  46563  fperdvper  46603  dvbdfbdioolem2  46613  dvnmul  46627  itgsinexp  46639  itgperiod  46665  stoweidlem11  46695  stoweidlem14  46698  stoweidlem26  46710  stoweidlem34  46718  wallispilem5  46753  stirlinglem5  46762  stirlinglem11  46768  stirlinglem12  46769  dirkercncflem1  46787  fourierdlem11  46802  fourierdlem15  46806  fourierdlem26  46817  fourierdlem41  46832  fourierdlem42  46833  fourierdlem48  46838  fourierdlem49  46839  fourierdlem63  46853  fourierdlem64  46854  fourierdlem65  46855  fourierdlem74  46864  fourierdlem75  46865  fourierdlem79  46869  fourierdlem81  46871  fourierdlem84  46874  fourierdlem88  46878  fourierdlem90  46880  fourierdlem92  46882  fourierdlem95  46885  fourierdlem97  46887  fourierdlem103  46893  fourierdlem104  46894  fourierdlem109  46899  fourierdlem111  46901  fourierswlem  46914  fouriersw  46915  elaa2lem  46917  etransclem23  46941  etransclem24  46942  etransclem28  46946  etransclem38  46956  smfmullem1  47475  m1modmmod  48068  fargshiftfo  48158  lighneallem3  48326  nnsum4primeseven  48532  nnsum4primesevenALTV  48533  bgoldbtbndlem4  48540  bgoldbtbnd  48541  gpgedgvtx1  48794  dignn0flhalflem1  49362  affineid  49451  eenglngeehlnmlem1  49484  itsclquadb  49523