Theorem npcand 11613

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

Syntax hints:   → wi 4   = wceq 1533   ∈ wcel 2098  (class class class)co 7426  ℂcc 11144   + caddc 11149   − cmin 11482

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-10 2129  ax-11 2146  ax-12 2166  ax-ext 2699  ax-sep 5303  ax-nul 5310  ax-pow 5369  ax-pr 5433  ax-un 7746  ax-resscn 11203  ax-1cn 11204  ax-icn 11205  ax-addcl 11206  ax-addrcl 11207  ax-mulcl 11208  ax-mulrcl 11209  ax-mulcom 11210  ax-addass 11211  ax-mulass 11212  ax-distr 11213  ax-i2m1 11214  ax-1ne0 11215  ax-1rid 11216  ax-rnegex 11217  ax-rrecex 11218  ax-cnre 11219  ax-pre-lttri 11220  ax-pre-lttrn 11221  ax-pre-ltadd 11222

This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-3or 1085  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-nf 1778  df-sb 2060  df-mo 2529  df-eu 2558  df-clab 2706  df-cleq 2720  df-clel 2806  df-nfc 2881  df-ne 2938  df-nel 3044  df-ral 3059  df-rex 3068  df-reu 3375  df-rab 3431  df-v 3475  df-sbc 3779  df-csb 3895  df-dif 3952  df-un 3954  df-in 3956  df-ss 3966  df-nul 4327  df-if 4533  df-pw 4608  df-sn 4633  df-pr 4635  df-op 4639  df-uni 4913  df-br 5153  df-opab 5215  df-mpt 5236  df-id 5580  df-po 5594  df-so 5595  df-xp 5688  df-rel 5689  df-cnv 5690  df-co 5691  df-dm 5692  df-rn 5693  df-res 5694  df-ima 5695  df-iota 6505  df-fun 6555  df-fn 6556  df-f 6557  df-f1 6558  df-fo 6559  df-f1o 6560  df-fv 6561  df-riota 7382  df-ov 7429  df-oprab 7430  df-mpo 7431  df-er 8731  df-en 8971  df-dom 8972  df-sdom 8973  df-pnf 11288  df-mnf 11289  df-ltxr 11291  df-sub 11484

This theorem is referenced by:  addlsub  11668  npcan1  11677  ltsubadd  11722  lesubadd  11724  lesub1  11746  lincmb01cmp  13512  expaddzlem  14110  bcpasc  14320  bcn2m1  14323  cshwidxmod  14793  repswcshw  14802  swrds2m  14932  shftuz  15056  o1dif  15614  arisum2  15847  ntrivcvg  15883  ntrivcvgtail  15886  prodrblem  15913  fprodser  15933  fprodm1  15951  risefacval2  15994  fallfacval2  15995  fallfacfwd  16020  binomfallfaclem2  16024  sin01bnd  16169  moddvds  16249  dvdsexp  16312  bitscmp  16420  hashdvds  16751  vdwlem5  16961  vdwlem6  16962  vdwlem8  16964  srgbinomlem4  20176  freshmansdream  21515  psdmul  22097  uniioombllem3  25534  i1faddlem  25642  itg1addlem4  25648  itg1addlem4OLD  25649  dvcnp2  25869  dvcnp2OLD  25870  ftc1lem4  25994  dgrcolem2  26229  plydivlem4  26251  aaliou3lem8  26300  dvtaylp  26325  dvntaylp0  26327  taylthlem1  26328  efif1olem4  26499  tanarg  26573  quart1  26808  dmgmaddnn0  26979  lgamgulm2  26988  gamfac  27019  basellem9  27041  chtublem  27164  logexprlim  27178  dchrptlem1  27217  lgsquadlem1  27333  mudivsum  27483  logsqvma  27495  log2sumbnd  27497  selberglem2  27499  pntrlog2bndlem5  27534  pntlem3  27562  ostth2lem2  27587  brbtwn2  28736  cusgrsize2inds  29287  clwlkclwwlklem2  29830  clwwisshclwws  29845  clwwlkel  29876  clwwlkf  29877  clwwlknonex2lem1  29937  2clwwlk2clwwlk  30180  numclwwlk2  30211  fzspl  32579  fzsplit3  32583  bcm1n  32584  wrdt2ind  32695  swrdrn3  32697  omndmul3  32814  psgnfzto1stlem  32842  cycpmco2lem5  32872  cycpmco2lem6  32873  ballotlemfc0  34145  ballotlemfcc  34146  signstfvn  34234  reprsuc  34280  breprexplemc  34297  lpadlen2  34346  revwlk  34767  bcm1nt  35364  itg2addnclem  37177  ftc1cnnclem  37197  ftc1anc  37207  caushft  37267  fzsplitnd  41485  lcmfunnnd  41515  lcmineqlem4  41535  lcmineqlem23  41554  intlewftc  41564  dvle2  41575  primrootsunit1  41599  aks6d1c5lem3  41640  aks6d1c5lem2  41641  sticksstones10  41659  sticksstones12a  41661  sticksstones16  41666  metakunt8  41696  nicomachus  41903  fltnltalem  42117  pellexlem6  42285  rmspecfund  42360  rmyluc  42389  jm2.18  42440  jm2.25  42451  hbtlem4  42581  bccm1k  43810  binomcxplemwb  43816  binomcxplemnotnn0  43824  oddfl  44688  zltlesub  44696  fzisoeu  44711  fperiodmul  44715  fzdifsuc2  44721  iccshift  44932  iooshift  44936  fmul01lt1lem2  45002  limcperiod  45045  sumnnodd  45047  cncfperiod  45296  fperdvper  45336  dvbdfbdioolem2  45346  dvnmul  45360  itgsinexp  45372  itgperiod  45398  stoweidlem11  45428  stoweidlem14  45431  stoweidlem26  45443  stoweidlem34  45451  wallispilem5  45486  stirlinglem5  45495  stirlinglem11  45501  stirlinglem12  45502  dirkercncflem1  45520  fourierdlem11  45535  fourierdlem15  45539  fourierdlem26  45550  fourierdlem41  45565  fourierdlem42  45566  fourierdlem48  45571  fourierdlem49  45572  fourierdlem63  45586  fourierdlem64  45587  fourierdlem65  45588  fourierdlem74  45597  fourierdlem75  45598  fourierdlem79  45602  fourierdlem81  45604  fourierdlem84  45607  fourierdlem88  45611  fourierdlem90  45613  fourierdlem92  45615  fourierdlem95  45618  fourierdlem97  45620  fourierdlem103  45626  fourierdlem104  45627  fourierdlem109  45632  fourierdlem111  45634  fourierswlem  45647  fouriersw  45648  elaa2lem  45650  etransclem23  45674  etransclem24  45675  etransclem28  45679  etransclem38  45689  smfmullem1  46208  fargshiftfo  46811  lighneallem3  46976  nnsum4primeseven  47169  nnsum4primesevenALTV  47170  bgoldbtbndlem4  47177  bgoldbtbnd  47178  m1modmmod  47672  dignn0flhalflem1  47766  affineid  47855  eenglngeehlnmlem1  47888  itsclquadb  47927