Theorem npcand 11001

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

Syntax hints:   → wi 4   = wceq 1537   ∈ wcel 2114  (class class class)co 7156  ℂcc 10535   + caddc 10540   − cmin 10870

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 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2793  ax-sep 5203  ax-nul 5210  ax-pow 5266  ax-pr 5330  ax-un 7461  ax-resscn 10594  ax-1cn 10595  ax-icn 10596  ax-addcl 10597  ax-addrcl 10598  ax-mulcl 10599  ax-mulrcl 10600  ax-mulcom 10601  ax-addass 10602  ax-mulass 10603  ax-distr 10604  ax-i2m1 10605  ax-1ne0 10606  ax-1rid 10607  ax-rnegex 10608  ax-rrecex 10609  ax-cnre 10610  ax-pre-lttri 10611  ax-pre-lttrn 10612  ax-pre-ltadd 10613

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3or 1084  df-3an 1085  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-mo 2622  df-eu 2654  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-ne 3017  df-nel 3124  df-ral 3143  df-rex 3144  df-reu 3145  df-rab 3147  df-v 3496  df-sbc 3773  df-csb 3884  df-dif 3939  df-un 3941  df-in 3943  df-ss 3952  df-nul 4292  df-if 4468  df-pw 4541  df-sn 4568  df-pr 4570  df-op 4574  df-uni 4839  df-br 5067  df-opab 5129  df-mpt 5147  df-id 5460  df-po 5474  df-so 5475  df-xp 5561  df-rel 5562  df-cnv 5563  df-co 5564  df-dm 5565  df-rn 5566  df-res 5567  df-ima 5568  df-iota 6314  df-fun 6357  df-fn 6358  df-f 6359  df-f1 6360  df-fo 6361  df-f1o 6362  df-fv 6363  df-riota 7114  df-ov 7159  df-oprab 7160  df-mpo 7161  df-er 8289  df-en 8510  df-dom 8511  df-sdom 8512  df-pnf 10677  df-mnf 10678  df-ltxr 10680  df-sub 10872

This theorem is referenced by:  addlsub  11056  npcan1  11065  ltsubadd  11110  lesubadd  11112  lesub1  11134  lincmb01cmp  12882  expaddzlem  13473  bcpasc  13682  bcn2m1  13685  cshwidxmod  14165  repswcshw  14174  swrds2m  14303  shftuz  14428  o1dif  14986  arisum2  15216  ntrivcvg  15253  ntrivcvgtail  15256  prodrblem  15283  fprodser  15303  fprodm1  15321  risefacval2  15364  fallfacval2  15365  fallfacfwd  15390  binomfallfaclem2  15394  sin01bnd  15538  moddvds  15618  dvdsexp  15677  bitscmp  15787  hashdvds  16112  vdwlem5  16321  vdwlem6  16322  vdwlem8  16324  srgbinomlem4  19293  uniioombllem3  24186  i1faddlem  24294  itg1addlem4  24300  dvcnp2  24517  ftc1lem4  24636  dgrcolem2  24864  plydivlem4  24885  aaliou3lem8  24934  dvtaylp  24958  dvntaylp0  24960  taylthlem1  24961  efif1olem4  25129  tanarg  25202  quart1  25434  dmgmaddnn0  25604  lgamgulm2  25613  gamfac  25644  basellem9  25666  chtublem  25787  logexprlim  25801  dchrptlem1  25840  lgsquadlem1  25956  mudivsum  26106  logsqvma  26118  log2sumbnd  26120  selberglem2  26122  pntrlog2bndlem5  26157  pntlem3  26185  ostth2lem2  26210  brbtwn2  26691  cusgrsize2inds  27235  clwlkclwwlklem2  27778  clwwisshclwws  27793  clwwlkel  27825  clwwlkf  27826  clwwlknonex2lem1  27886  2clwwlk2clwwlk  28129  numclwwlk2  28160  fzspl  30513  fzsplit3  30517  bcm1n  30518  wrdt2ind  30627  swrdrn3  30629  omndmul3  30714  psgnfzto1stlem  30742  cycpmco2lem5  30772  cycpmco2lem6  30773  freshmansdream  30859  ballotlemfc0  31750  ballotlemfcc  31751  signstfvn  31839  reprsuc  31886  breprexplemc  31903  lpadlen2  31952  revwlk  32371  bcm1nt  32969  itg2addnclem  34958  ftc1cnnclem  34980  ftc1anc  34990  caushft  35051  lcmfunnnd  39133  fltnltalem  39323  pellexlem6  39480  rmspecfund  39555  rmyluc  39583  jm2.18  39634  jm2.25  39645  hbtlem4  39775  bccm1k  40723  binomcxplemwb  40729  binomcxplemnotnn0  40737  oddfl  41592  zltlesub  41600  fzisoeu  41616  fperiodmul  41620  fzdifsuc2  41626  iccshift  41843  iooshift  41847  fmul01lt1lem2  41915  limcperiod  41958  sumnnodd  41960  cncfperiod  42211  fperdvper  42252  dvbdfbdioolem2  42263  dvnmul  42277  itgsinexp  42289  itgperiod  42315  stoweidlem11  42345  stoweidlem14  42348  stoweidlem26  42360  stoweidlem34  42368  wallispilem5  42403  stirlinglem5  42412  stirlinglem11  42418  stirlinglem12  42419  dirkercncflem1  42437  fourierdlem11  42452  fourierdlem15  42456  fourierdlem26  42467  fourierdlem41  42482  fourierdlem42  42483  fourierdlem48  42488  fourierdlem49  42489  fourierdlem63  42503  fourierdlem64  42504  fourierdlem65  42505  fourierdlem74  42514  fourierdlem75  42515  fourierdlem79  42519  fourierdlem81  42521  fourierdlem84  42524  fourierdlem88  42528  fourierdlem90  42530  fourierdlem92  42532  fourierdlem95  42535  fourierdlem97  42537  fourierdlem103  42543  fourierdlem104  42544  fourierdlem109  42549  fourierdlem111  42551  fourierswlem  42564  fouriersw  42565  elaa2lem  42567  etransclem23  42591  etransclem24  42592  etransclem28  42596  etransclem38  42606  smfmullem1  43115  fargshiftfo  43651  lighneallem3  43821  nnsum4primeseven  44014  nnsum4primesevenALTV  44015  bgoldbtbndlem4  44022  bgoldbtbnd  44023  m1modmmod  44630  dignn0flhalflem1  44724  affineid  44740  eenglngeehlnmlem1  44773  itsclquadb  44812