Theorem npcand 11319

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

Syntax hints:   → wi 4   = wceq 1541   ∈ wcel 2109  (class class class)co 7268  ℂcc 10853   + caddc 10858   − cmin 11188

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1801  ax-4 1815  ax-5 1916  ax-6 1974  ax-7 2014  ax-8 2111  ax-9 2119  ax-10 2140  ax-11 2157  ax-12 2174  ax-ext 2710  ax-sep 5226  ax-nul 5233  ax-pow 5291  ax-pr 5355  ax-un 7579  ax-resscn 10912  ax-1cn 10913  ax-icn 10914  ax-addcl 10915  ax-addrcl 10916  ax-mulcl 10917  ax-mulrcl 10918  ax-mulcom 10919  ax-addass 10920  ax-mulass 10921  ax-distr 10922  ax-i2m1 10923  ax-1ne0 10924  ax-1rid 10925  ax-rnegex 10926  ax-rrecex 10927  ax-cnre 10928  ax-pre-lttri 10929  ax-pre-lttrn 10930  ax-pre-ltadd 10931

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-3or 1086  df-3an 1087  df-tru 1544  df-fal 1554  df-ex 1786  df-nf 1790  df-sb 2071  df-mo 2541  df-eu 2570  df-clab 2717  df-cleq 2731  df-clel 2817  df-nfc 2890  df-ne 2945  df-nel 3051  df-ral 3070  df-rex 3071  df-reu 3072  df-rab 3074  df-v 3432  df-sbc 3720  df-csb 3837  df-dif 3894  df-un 3896  df-in 3898  df-ss 3908  df-nul 4262  df-if 4465  df-pw 4540  df-sn 4567  df-pr 4569  df-op 4573  df-uni 4845  df-br 5079  df-opab 5141  df-mpt 5162  df-id 5488  df-po 5502  df-so 5503  df-xp 5594  df-rel 5595  df-cnv 5596  df-co 5597  df-dm 5598  df-rn 5599  df-res 5600  df-ima 5601  df-iota 6388  df-fun 6432  df-fn 6433  df-f 6434  df-f1 6435  df-fo 6436  df-f1o 6437  df-fv 6438  df-riota 7225  df-ov 7271  df-oprab 7272  df-mpo 7273  df-er 8472  df-en 8708  df-dom 8709  df-sdom 8710  df-pnf 10995  df-mnf 10996  df-ltxr 10998  df-sub 11190

This theorem is referenced by:  addlsub  11374  npcan1  11383  ltsubadd  11428  lesubadd  11430  lesub1  11452  lincmb01cmp  13209  expaddzlem  13807  bcpasc  14016  bcn2m1  14019  cshwidxmod  14497  repswcshw  14506  swrds2m  14635  shftuz  14761  o1dif  15320  arisum2  15554  ntrivcvg  15590  ntrivcvgtail  15593  prodrblem  15620  fprodser  15640  fprodm1  15658  risefacval2  15701  fallfacval2  15702  fallfacfwd  15727  binomfallfaclem2  15731  sin01bnd  15875  moddvds  15955  dvdsexp  16018  bitscmp  16126  hashdvds  16457  vdwlem5  16667  vdwlem6  16668  vdwlem8  16670  srgbinomlem4  19760  uniioombllem3  24730  i1faddlem  24838  itg1addlem4  24844  itg1addlem4OLD  24845  dvcnp2  25065  ftc1lem4  25184  dgrcolem2  25416  plydivlem4  25437  aaliou3lem8  25486  dvtaylp  25510  dvntaylp0  25512  taylthlem1  25513  efif1olem4  25682  tanarg  25755  quart1  25987  dmgmaddnn0  26157  lgamgulm2  26166  gamfac  26197  basellem9  26219  chtublem  26340  logexprlim  26354  dchrptlem1  26393  lgsquadlem1  26509  mudivsum  26659  logsqvma  26671  log2sumbnd  26673  selberglem2  26675  pntrlog2bndlem5  26710  pntlem3  26738  ostth2lem2  26763  brbtwn2  27254  cusgrsize2inds  27801  clwlkclwwlklem2  28343  clwwisshclwws  28358  clwwlkel  28389  clwwlkf  28390  clwwlknonex2lem1  28450  2clwwlk2clwwlk  28693  numclwwlk2  28724  fzspl  31090  fzsplit3  31094  bcm1n  31095  wrdt2ind  31204  swrdrn3  31206  omndmul3  31318  psgnfzto1stlem  31346  cycpmco2lem5  31376  cycpmco2lem6  31377  freshmansdream  31463  ballotlemfc0  32438  ballotlemfcc  32439  signstfvn  32527  reprsuc  32574  breprexplemc  32591  lpadlen2  32640  revwlk  33065  bcm1nt  33682  itg2addnclem  35807  ftc1cnnclem  35827  ftc1anc  35837  caushft  35898  fzsplitnd  39971  lcmfunnnd  40000  lcmineqlem4  40020  lcmineqlem23  40039  intlewftc  40049  dvle2  40060  sticksstones10  40091  sticksstones12a  40093  sticksstones16  40098  metakunt8  40112  fltnltalem  40479  pellexlem6  40636  rmspecfund  40711  rmyluc  40739  jm2.18  40790  jm2.25  40801  hbtlem4  40931  bccm1k  41913  binomcxplemwb  41919  binomcxplemnotnn0  41927  oddfl  42769  zltlesub  42777  fzisoeu  42793  fperiodmul  42797  fzdifsuc2  42803  iccshift  43010  iooshift  43014  fmul01lt1lem2  43080  limcperiod  43123  sumnnodd  43125  cncfperiod  43374  fperdvper  43414  dvbdfbdioolem2  43424  dvnmul  43438  itgsinexp  43450  itgperiod  43476  stoweidlem11  43506  stoweidlem14  43509  stoweidlem26  43521  stoweidlem34  43529  wallispilem5  43564  stirlinglem5  43573  stirlinglem11  43579  stirlinglem12  43580  dirkercncflem1  43598  fourierdlem11  43613  fourierdlem15  43617  fourierdlem26  43628  fourierdlem41  43643  fourierdlem42  43644  fourierdlem48  43649  fourierdlem49  43650  fourierdlem63  43664  fourierdlem64  43665  fourierdlem65  43666  fourierdlem74  43675  fourierdlem75  43676  fourierdlem79  43680  fourierdlem81  43682  fourierdlem84  43685  fourierdlem88  43689  fourierdlem90  43691  fourierdlem92  43693  fourierdlem95  43696  fourierdlem97  43698  fourierdlem103  43704  fourierdlem104  43705  fourierdlem109  43710  fourierdlem111  43712  fourierswlem  43725  fouriersw  43726  elaa2lem  43728  etransclem23  43752  etransclem24  43753  etransclem28  43757  etransclem38  43767  smfmullem1  44276  fargshiftfo  44846  lighneallem3  45011  nnsum4primeseven  45204  nnsum4primesevenALTV  45205  bgoldbtbndlem4  45212  bgoldbtbnd  45213  m1modmmod  45819  dignn0flhalflem1  45913  affineid  46002  eenglngeehlnmlem1  46035  itsclquadb  46074