Theorem npcand 11674

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

This proof depends on syntax axioms:   → wi 4   = wceq 1569   ∈ wcel 2144  (class class class)co 7420  ℂcc 11199   + caddc 11204   − cmin 11542

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-10 2177  ax-11 2193  ax-12 2212  ax-ext 2732  ax-sep 5248  ax-nul 5259  ax-pow 5326  ax-pr 5390  ax-un 7751  ax-resscn 11258  ax-1cn 11259  ax-icn 11260  ax-addcl 11261  ax-addrcl 11262  ax-mulcl 11263  ax-mulrcl 11264  ax-mulcom 11265  ax-addass 11266  ax-mulass 11267  ax-distr 11268  ax-i2m1 11269  ax-1ne0 11270  ax-1rid 11271  ax-rnegex 11272  ax-rrecex 11273  ax-cnre 11274  ax-pre-lttri 11275  ax-pre-lttrn 11276  ax-pre-ltadd 11277

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-nf 1816  df-sb 2099  df-mo 2564  df-eu 2594  df-clab 2739  df-cleq 2752  df-clel 2835  df-nfc 2909  df-ne 2956  df-nel 3062  df-ral 3077  df-rex 3087  df-reu 3366  df-rab 3413  df-v 3452  df-sbc 3739  df-csb 3847  df-ss 3896  df-dif 4047  df-in 4091  df-un 4151  df-nul 4279  df-if 4482  df-pw 4558  df-sn 4584  df-pr 4586  df-op 4590  df-uni 4867  df-br 5103  df-opab 5167  df-mpt 5186  df-id 5545  df-po 5558  df-so 5559  df-xp 5656  df-rel 5657  df-cnv 5658  df-co 5659  df-dm 5660  df-rn 5661  df-res 5662  df-ima 5663  df-iota 6494  df-fun 6540  df-fn 6541  df-f 6542  df-f1 6543  df-fo 6544  df-f1o 6545  df-fv 6546  df-riota 7377  df-ov 7423  df-oprab 7424  df-mpo 7425  df-er 8718  df-en 8975  df-dom 8976  df-sdom 8977  df-pnf 11346  df-mnf 11347  df-ltxr 11349  df-sub 11544

This theorem is used by:  addlsub  11733  npcan1  11742  ltsubadd  11787  lesubadd  11789  lesub1  11811  lincmb01cmp  13627  bcpasc  14466  bcn2m1  14469  swrdrn3  14803  cshwidxmod  14955  repswcshw  14964  swrds2m  15093  shftuz  15223  o1dif  15798  arisum2  16031  ntrivcvg  16067  ntrivcvgtail  16070  prodrblem  16097  fprodser  16117  fprodm1  16135  risefacval2  16178  fallfacval2  16179  fallfacfwd  16203  binomfallfaclem2  16207  sin01bnd  16354  moddvds  16434  dvdsexp  16499  bitscmp  16609  hashdvds  16953  vdwlem5  17164  vdwlem6  17165  vdwlem8  17167  chnrev  18802  omndmul3  20349  srgbinomlem4  20456  freshmansdream  21881  psdmul  22488  uniioombllem3  25907  i1faddlem  26015  itg1addlem4  26021  dvcnp2  26241  ftc1lem4  26360  dgrcolem2  26594  plydivlem4  26618  aaliou3lem8  26673  dvtaylp  26698  dvntaylp0  26700  taylthlem1  26701  tanarg  26948  quart1  27185  dmgmaddnn0  27355  lgamgulm2  27364  gamfac  27395  basellem9  27417  chtublem  27539  logexprlim  27553  dchrptlem1  27592  lgsquadlem1  27708  mudivsum  27858  logsqvma  27870  log2sumbnd  27872  selberglem2  27874  pntrlog2bndlem5  27909  pntlem3  27937  ostth2lem2  27962  brbtwn2  29484  cusgrsize2inds  30035  revwlk  30268  clwlkclwwlklem2  30592  clwwisshclwws  30607  clwwlkel  30638  clwwlkf  30639  clwwlknonex2lem1  30699  2clwwlk2clwwlk  30952  numclwwlk2  30983  fzspl  33424  fzsplit3  33428  bcm1n  33430  oexpled  33470  wrdt2ind  33559  psgnfzto1stlem  33704  cycpmco2lem5  33734  cycpmco2lem6  33735  esplyfvn  34252  vietalem  34254  ballotlemfc0  35168  ballotlemfcc  35169  signstfvn  35241  reprsuc  35287  breprexplemc  35304  lpadlen2  35356  bcm1nt  36577  itg2addnclem  38665  ftc1cnnclem  38685  ftc1anc  38695  caushft  38771  fzsplitnd  43108  lcmfunnnd  43138  lcmineqlem4  43158  lcmineqlem23  43177  intlewftc  43187  dvle2  43198  primrootsunit1  43223  aks6d1c5lem3  43263  aks6d1c5lem2  43264  sticksstones10  43281  sticksstones12a  43283  sticksstones16  43288  unitscyglem5  43325  nicomachus  43445  fltnltalem  43749  pellexlem6  43917  rmspecfund  43992  rmyluc  44020  jm2.18  44071  jm2.25  44082  hbtlem4  44204  bccm1k  45402  binomcxplemwb  45408  binomcxplemnotnn0  45416  oddfl  46370  zltlesub  46377  fperiodmul  46396  fzdifsuc2  46402  iccshift  46606  iooshift  46610  fmul01lt1lem2  46673  limcperiod  46716  sumnnodd  46718  cncfperiod  46965  fperdvper  47005  dvbdfbdioolem2  47015  dvnmul  47029  itgsinexp  47041  itgperiod  47067  stoweidlem11  47097  stoweidlem14  47100  stoweidlem26  47112  stoweidlem34  47120  wallispilem5  47155  stirlinglem5  47164  stirlinglem11  47170  stirlinglem12  47171  dirkercncflem1  47189  fourierdlem11  47204  fourierdlem15  47208  fourierdlem26  47219  fourierdlem41  47234  fourierdlem42  47235  fourierdlem48  47240  fourierdlem49  47241  fourierdlem63  47255  fourierdlem64  47256  fourierdlem65  47257  fourierdlem74  47266  fourierdlem75  47267  fourierdlem79  47271  fourierdlem81  47273  fourierdlem84  47276  fourierdlem88  47280  fourierdlem90  47282  fourierdlem92  47284  fourierdlem95  47287  fourierdlem97  47289  fourierdlem103  47295  fourierdlem104  47296  fourierdlem109  47301  fourierdlem111  47303  fourierswlem  47316  fouriersw  47317  elaa2lem  47319  etransclem23  47343  etransclem24  47344  etransclem28  47348  etransclem38  47358  smfmullem1  47877  m1modmmod  48510  fargshiftfo  48600  lighneallem3  48768  nnsum4primeseven  48974  nnsum4primesevenALTV  48975  bgoldbtbndlem4  48982  bgoldbtbnd  48983  gpgedgvtx1  49236  dignn0flhalflem1  49803  affineid  49892  eenglngeehlnmlem1  49925  itsclquadb  49964