Theorem npcand 11600

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

This proof depends on syntax axioms:   → wi 4   = wceq 1570   ∈ wcel 2145  (class class class)co 7416  ℂcc 11125   + caddc 11130   − cmin 11468

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 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2215  ax-ext 2734  ax-sep 5255  ax-nul 5267  ax-pow 5334  ax-pr 5402  ax-un 7739  ax-resscn 11184  ax-1cn 11185  ax-icn 11186  ax-addcl 11187  ax-addrcl 11188  ax-mulcl 11189  ax-mulrcl 11190  ax-mulcom 11191  ax-addass 11192  ax-mulass 11193  ax-distr 11194  ax-i2m1 11195  ax-1ne0 11196  ax-1rid 11197  ax-rnegex 11198  ax-rrecex 11199  ax-cnre 11200  ax-pre-lttri 11201  ax-pre-lttrn 11202  ax-pre-ltadd 11203

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 2100  df-mo 2566  df-eu 2596  df-clab 2741  df-cleq 2754  df-clel 2837  df-nfc 2911  df-ne 2958  df-nel 3064  df-ral 3079  df-rex 3089  df-reu 3368  df-rab 3415  df-v 3455  df-sbc 3743  df-csb 3851  df-dif 3905  df-un 3907  df-in 3909  df-ss 3919  df-nul 4283  df-if 4486  df-pw 4562  df-sn 4588  df-pr 4590  df-op 4594  df-uni 4871  df-br 5108  df-opab 5172  df-mpt 5191  df-id 5554  df-po 5567  df-so 5568  df-xp 5665  df-rel 5666  df-cnv 5667  df-co 5668  df-dm 5669  df-rn 5670  df-res 5671  df-ima 5672  df-iota 6493  df-fun 6539  df-fn 6540  df-f 6541  df-f1 6542  df-fo 6543  df-f1o 6544  df-fv 6545  df-riota 7373  df-ov 7419  df-oprab 7420  df-mpo 7421  df-er 8699  df-en 8956  df-dom 8957  df-sdom 8958  df-pnf 11272  df-mnf 11273  df-ltxr 11275  df-sub 11470

This theorem is used by:  addlsub  11657  npcan1  11666  ltsubadd  11711  lesubadd  11713  lesub1  11735  lincmb01cmp  13550  expaddzlem  14171  bcpasc  14387  bcn2m1  14390  swrdrn3  14724  cshwidxmod  14876  repswcshw  14885  swrds2m  15014  shftuz  15144  o1dif  15719  arisum2  15952  ntrivcvg  15988  ntrivcvgtail  15991  prodrblem  16020  fprodser  16040  fprodm1  16058  risefacval2  16101  fallfacval2  16102  fallfacfwd  16126  binomfallfaclem2  16130  sin01bnd  16277  moddvds  16357  dvdsexp  16422  bitscmp  16532  hashdvds  16870  vdwlem5  17081  vdwlem6  17082  vdwlem8  17084  chnrev  18719  omndmul3  20265  srgbinomlem4  20372  freshmansdream  21791  psdmul  22398  uniioombllem3  25817  i1faddlem  25925  itg1addlem4  25931  dvcnp2  26152  ftc1lem4  26271  dgrcolem2  26504  plydivlem4  26530  aaliou3lem8  26581  dvtaylp  26606  dvntaylp0  26608  taylthlem1  26609  efif1olem4  26783  tanarg  26857  quart1  27094  dmgmaddnn0  27264  lgamgulm2  27273  gamfac  27304  basellem9  27326  chtublem  27448  logexprlim  27462  dchrptlem1  27501  lgsquadlem1  27617  mudivsum  27767  logsqvma  27779  log2sumbnd  27781  selberglem2  27783  pntrlog2bndlem5  27818  pntlem3  27846  ostth2lem2  27871  brbtwn2  29363  cusgrsize2inds  29914  revwlk  30147  clwlkclwwlklem2  30471  clwwisshclwws  30486  clwwlkel  30517  clwwlkf  30518  clwwlknonex2lem1  30578  2clwwlk2clwwlk  30831  numclwwlk2  30862  fzspl  33262  fzsplit3  33266  bcm1n  33268  oexpled  33308  wrdt2ind  33397  psgnfzto1stlem  33542  cycpmco2lem5  33572  cycpmco2lem6  33573  esplyfvn  34089  vietalem  34091  ballotlemfc0  35006  ballotlemfcc  35007  signstfvn  35079  reprsuc  35125  breprexplemc  35142  lpadlen2  35194  bcm1nt  36318  itg2addnclem  38422  ftc1cnnclem  38442  ftc1anc  38452  caushft  38513  fzsplitnd  42850  lcmfunnnd  42880  lcmineqlem4  42900  lcmineqlem23  42919  intlewftc  42929  dvle2  42940  primrootsunit1  42965  aks6d1c5lem3  43005  aks6d1c5lem2  43006  sticksstones10  43023  sticksstones12a  43025  sticksstones16  43030  unitscyglem5  43067  nicomachus  43189  fltnltalem  43510  pellexlem6  43677  rmspecfund  43752  rmyluc  43780  jm2.18  43831  jm2.25  43842  hbtlem4  43969  bccm1k  45168  binomcxplemwb  45174  binomcxplemnotnn0  45182  oddfl  46113  zltlesub  46120  fzisoeu  46135  fperiodmul  46139  fzdifsuc2  46145  iccshift  46350  iooshift  46354  fmul01lt1lem2  46417  limcperiod  46460  sumnnodd  46462  cncfperiod  46709  fperdvper  46749  dvbdfbdioolem2  46759  dvnmul  46773  itgsinexp  46785  itgperiod  46811  stoweidlem11  46841  stoweidlem14  46844  stoweidlem26  46856  stoweidlem34  46864  wallispilem5  46899  stirlinglem5  46908  stirlinglem11  46914  stirlinglem12  46915  dirkercncflem1  46933  fourierdlem11  46948  fourierdlem15  46952  fourierdlem26  46963  fourierdlem41  46978  fourierdlem42  46979  fourierdlem48  46984  fourierdlem49  46985  fourierdlem63  46999  fourierdlem64  47000  fourierdlem65  47001  fourierdlem74  47010  fourierdlem75  47011  fourierdlem79  47015  fourierdlem81  47017  fourierdlem84  47020  fourierdlem88  47024  fourierdlem90  47026  fourierdlem92  47028  fourierdlem95  47031  fourierdlem97  47033  fourierdlem103  47039  fourierdlem104  47040  fourierdlem109  47045  fourierdlem111  47047  fourierswlem  47060  fouriersw  47061  elaa2lem  47063  etransclem23  47087  etransclem24  47088  etransclem28  47092  etransclem38  47102  smfmullem1  47621  m1modmmod  48254  fargshiftfo  48344  lighneallem3  48512  nnsum4primeseven  48718  nnsum4primesevenALTV  48719  bgoldbtbndlem4  48726  bgoldbtbnd  48727  gpgedgvtx1  48980  dignn0flhalflem1  49547  affineid  49636  eenglngeehlnmlem1  49669  itsclquadb  49708