Theorem npcand 11700

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

This proof depends on syntax axioms:   → wi 4   = wceq 1570   ∈ wcel 2147  (class class class)co 7443  ℂcc 11225   + caddc 11230   − cmin 11568

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-10 2180  ax-11 2197  ax-12 2216  ax-ext 2735  ax-sep 5252  ax-nul 5263  ax-pow 5331  ax-pr 5395  ax-un 7775  ax-resscn 11284  ax-1cn 11285  ax-icn 11286  ax-addcl 11287  ax-addrcl 11288  ax-mulcl 11289  ax-mulrcl 11290  ax-mulcom 11291  ax-addass 11292  ax-mulass 11293  ax-distr 11294  ax-i2m1 11295  ax-1ne0 11296  ax-1rid 11297  ax-rnegex 11298  ax-rrecex 11299  ax-cnre 11300  ax-pre-lttri 11301  ax-pre-lttrn 11302  ax-pre-ltadd 11303

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2102  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2839  df-nfc 2913  df-ne 2960  df-nel 3066  df-ral 3081  df-rex 3091  df-reu 3370  df-rab 3417  df-v 3456  df-sbc 3743  df-csb 3852  df-ss 3901  df-dif 4050  df-in 4094  df-un 4154  df-nul 4282  df-if 4486  df-pw 4562  df-sn 4589  df-pr 4591  df-op 4839  df-uni 4871  df-br 5107  df-opab 5171  df-mpt 5190  df-id 5550  df-po 5563  df-so 5564  df-xp 5661  df-rel 5662  df-cnv 5663  df-co 5664  df-dm 5665  df-rn 5666  df-res 5667  df-ima 5668  df-iota 6512  df-fun 6560  df-fn 6561  df-f 6562  df-f1 6563  df-fo 6564  df-f1o 6565  df-fv 6566  df-riota 7400  df-ov 7446  df-oprab 7447  df-mpo 7448  df-er 8745  df-en 9002  df-dom 9003  df-sdom 9004  df-pnf 11372  df-mnf 11373  df-ltxr 11375  df-sub 11570

This theorem is used by:  addlsub  11759  npcan1  11768  ltsubadd  11813  lesubadd  11815  lesub1  11837  lincmb01cmp  13653  bcpasc  14492  bcn2m1  14495  swrdrn3  14830  cshwidxmod  14982  repswcshw  14991  swrds2m  15121  shftuz  15251  o1dif  15826  ntrivcvg  16095  ntrivcvgtail  16098  prodrblem  16125  fprodser  16145  fprodm1  16163  risefacval2  16206  fallfacval2  16207  fallfacfwd  16231  binomfallfaclem2  16235  sin01bnd  16382  moddvds  16462  dvdsexp  16527  bitscmp  16637  hashdvds  16981  vdwlem5  17192  vdwlem6  17193  vdwlem8  17195  chnrev  18830  omndmul3  20378  srgbinomlem4  20485  freshmansdream  21910  psdmul  22517  uniioombllem3  25936  i1faddlem  26044  itg1addlem4  26050  dvcnp2  26270  ftc1lem4  26389  dgrcolem2  26623  plydivlem4  26647  aaliou3lem8  26702  dvtaylp  26727  dvntaylp0  26729  taylthlem1  26730  tanarg  26977  quart1  27214  dmgmaddnn0  27384  lgamgulm2  27393  gamfac  27424  basellem9  27446  chtublem  27568  logexprlim  27582  dchrptlem1  27621  lgsquadlem1  27737  mudivsum  27887  logsqvma  27899  log2sumbnd  27901  selberglem2  27903  pntrlog2bndlem5  27938  pntlem3  27966  ostth2lem2  27991  brbtwn2  29513  cusgrsize2inds  30064  revwlk  30297  clwlkclwwlklem2  30621  clwwisshclwws  30636  clwwlkel  30667  clwwlkf  30668  clwwlknonex2lem1  30728  2clwwlk2clwwlk  30981  numclwwlk2  31012  fzspl  33451  fzsplit3  33455  bcm1n  33457  oexpled  33497  wrdt2ind  33586  psgnfzto1stlem  33731  cycpmco2lem5  33761  cycpmco2lem6  33762  esplyfvn  34279  vietalem  34281  ballotlemfc0  35195  ballotlemfcc  35196  signstfvn  35268  reprsuc  35314  breprexplemc  35331  lpadlen2  35383  bcm1nt  36680  itg2addnclem  38781  ftc1cnnclem  38801  ftc1anc  38811  caushft  38887  fzsplitnd  43224  lcmfunnnd  43254  lcmineqlem4  43274  lcmineqlem23  43293  intlewftc  43303  dvle2  43314  primrootsunit1  43339  aks6d1c5lem3  43379  aks6d1c5lem2  43380  sticksstones10  43397  sticksstones12a  43399  sticksstones16  43404  unitscyglem5  43441  nicomachus  43562  fltnltalem  43866  pellexlem6  44034  rmspecfund  44109  rmyluc  44137  jm2.18  44188  jm2.25  44199  hbtlem4  44320  bccm1k  45518  binomcxplemwb  45524  binomcxplemnotnn0  45532  oddfl  46499  zltlesub  46506  fperiodmul  46525  fzdifsuc2  46531  iccshift  46735  iooshift  46739  fmul01lt1lem2  46802  limcperiod  46845  sumnnodd  46847  cncfperiod  47094  fperdvper  47134  dvbdfbdioolem2  47144  dvnmul  47158  itgsinexp  47170  itgperiod  47196  stoweidlem11  47226  stoweidlem14  47229  stoweidlem26  47241  stoweidlem34  47249  wallispilem5  47284  stirlinglem5  47293  stirlinglem11  47299  stirlinglem12  47300  dirkercncflem1  47318  fourierdlem11  47333  fourierdlem15  47337  fourierdlem26  47348  fourierdlem41  47363  fourierdlem42  47364  fourierdlem48  47369  fourierdlem49  47370  fourierdlem63  47384  fourierdlem64  47385  fourierdlem65  47386  fourierdlem74  47395  fourierdlem75  47396  fourierdlem79  47400  fourierdlem81  47402  fourierdlem84  47405  fourierdlem88  47409  fourierdlem90  47411  fourierdlem92  47413  fourierdlem95  47416  fourierdlem97  47418  fourierdlem103  47424  fourierdlem104  47425  fourierdlem109  47430  fourierdlem111  47432  fourierswlem  47445  fouriersw  47446  elaa2lem  47448  etransclem23  47472  etransclem24  47473  etransclem28  47477  etransclem38  47487  smfmullem1  48006  m1modmmod  48639  fargshiftfo  48729  lighneallem3  48897  nnsum4primeseven  49103  nnsum4primesevenALTV  49104  bgoldbtbndlem4  49111  bgoldbtbnd  49112  gpgedgvtx1  49365  dignn0flhalflem1  49932  affineid  50021  eenglngeehlnmlem1  50055  itsclquadb  50093