Theorem npcand 11468

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

Syntax hints:   → wi 4   = wceq 1541   ∈ wcel 2110  (class class class)co 7341  ℂcc 10996   + caddc 11001   − cmin 11336

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 1968  ax-7 2009  ax-8 2112  ax-9 2120  ax-10 2143  ax-11 2159  ax-12 2179  ax-ext 2702  ax-sep 5232  ax-nul 5242  ax-pow 5301  ax-pr 5368  ax-un 7663  ax-resscn 11055  ax-1cn 11056  ax-icn 11057  ax-addcl 11058  ax-addrcl 11059  ax-mulcl 11060  ax-mulrcl 11061  ax-mulcom 11062  ax-addass 11063  ax-mulass 11064  ax-distr 11065  ax-i2m1 11066  ax-1ne0 11067  ax-1rid 11068  ax-rnegex 11069  ax-rrecex 11070  ax-cnre 11071  ax-pre-lttri 11072  ax-pre-lttrn 11073  ax-pre-ltadd 11074

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-nf 1785  df-sb 2067  df-mo 2534  df-eu 2563  df-clab 2709  df-cleq 2722  df-clel 2804  df-nfc 2879  df-ne 2927  df-nel 3031  df-ral 3046  df-rex 3055  df-reu 3345  df-rab 3394  df-v 3436  df-sbc 3740  df-csb 3849  df-dif 3903  df-un 3905  df-in 3907  df-ss 3917  df-nul 4282  df-if 4474  df-pw 4550  df-sn 4575  df-pr 4577  df-op 4581  df-uni 4858  df-br 5090  df-opab 5152  df-mpt 5171  df-id 5509  df-po 5522  df-so 5523  df-xp 5620  df-rel 5621  df-cnv 5622  df-co 5623  df-dm 5624  df-rn 5625  df-res 5626  df-ima 5627  df-iota 6433  df-fun 6479  df-fn 6480  df-f 6481  df-f1 6482  df-fo 6483  df-f1o 6484  df-fv 6485  df-riota 7298  df-ov 7344  df-oprab 7345  df-mpo 7346  df-er 8617  df-en 8865  df-dom 8866  df-sdom 8867  df-pnf 11140  df-mnf 11141  df-ltxr 11143  df-sub 11338

This theorem is referenced by:  addlsub  11525  npcan1  11534  ltsubadd  11579  lesubadd  11581  lesub1  11603  lincmb01cmp  13387  expaddzlem  14004  bcpasc  14220  bcn2m1  14223  cshwidxmod  14702  repswcshw  14711  swrds2m  14840  shftuz  14968  o1dif  15529  arisum2  15760  ntrivcvg  15796  ntrivcvgtail  15799  prodrblem  15828  fprodser  15848  fprodm1  15866  risefacval2  15909  fallfacval2  15910  fallfacfwd  15935  binomfallfaclem2  15939  sin01bnd  16086  moddvds  16166  dvdsexp  16231  bitscmp  16341  hashdvds  16678  vdwlem5  16889  vdwlem6  16890  vdwlem8  16892  chnrev  18525  omndmul3  20039  srgbinomlem4  20140  freshmansdream  21504  psdmul  22074  uniioombllem3  25506  i1faddlem  25614  itg1addlem4  25620  dvcnp2  25841  dvcnp2OLD  25842  ftc1lem4  25966  dgrcolem2  26200  plydivlem4  26224  aaliou3lem8  26273  dvtaylp  26298  dvntaylp0  26300  taylthlem1  26301  efif1olem4  26474  tanarg  26548  quart1  26786  dmgmaddnn0  26957  lgamgulm2  26966  gamfac  26997  basellem9  27019  chtublem  27142  logexprlim  27156  dchrptlem1  27195  lgsquadlem1  27311  mudivsum  27461  logsqvma  27473  log2sumbnd  27475  selberglem2  27477  pntrlog2bndlem5  27512  pntlem3  27540  ostth2lem2  27565  brbtwn2  28876  cusgrsize2inds  29425  clwlkclwwlklem2  29970  clwwisshclwws  29985  clwwlkel  30016  clwwlkf  30017  clwwlknonex2lem1  30077  2clwwlk2clwwlk  30320  numclwwlk2  30351  fzspl  32762  fzsplit3  32766  bcm1n  32767  oexpled  32820  wrdt2ind  32924  swrdrn3  32926  psgnfzto1stlem  33059  cycpmco2lem5  33089  cycpmco2lem6  33090  ballotlemfc0  34496  ballotlemfcc  34497  signstfvn  34572  reprsuc  34618  breprexplemc  34635  lpadlen2  34684  revwlk  35137  bcm1nt  35749  itg2addnclem  37690  ftc1cnnclem  37710  ftc1anc  37720  caushft  37780  fzsplitnd  41994  lcmfunnnd  42024  lcmineqlem4  42044  lcmineqlem23  42063  intlewftc  42073  dvle2  42084  primrootsunit1  42109  aks6d1c5lem3  42149  aks6d1c5lem2  42150  sticksstones10  42167  sticksstones12a  42169  sticksstones16  42174  unitscyglem5  42211  nicomachus  42324  fltnltalem  42674  pellexlem6  42846  rmspecfund  42921  rmyluc  42949  jm2.18  43000  jm2.25  43011  hbtlem4  43138  bccm1k  44354  binomcxplemwb  44360  binomcxplemnotnn0  44368  oddfl  45298  zltlesub  45305  fzisoeu  45320  fperiodmul  45324  fzdifsuc2  45330  iccshift  45537  iooshift  45541  fmul01lt1lem2  45604  limcperiod  45647  sumnnodd  45649  cncfperiod  45896  fperdvper  45936  dvbdfbdioolem2  45946  dvnmul  45960  itgsinexp  45972  itgperiod  45998  stoweidlem11  46028  stoweidlem14  46031  stoweidlem26  46043  stoweidlem34  46051  wallispilem5  46086  stirlinglem5  46095  stirlinglem11  46101  stirlinglem12  46102  dirkercncflem1  46120  fourierdlem11  46135  fourierdlem15  46139  fourierdlem26  46150  fourierdlem41  46165  fourierdlem42  46166  fourierdlem48  46171  fourierdlem49  46172  fourierdlem63  46186  fourierdlem64  46187  fourierdlem65  46188  fourierdlem74  46197  fourierdlem75  46198  fourierdlem79  46202  fourierdlem81  46204  fourierdlem84  46207  fourierdlem88  46211  fourierdlem90  46213  fourierdlem92  46215  fourierdlem95  46218  fourierdlem97  46220  fourierdlem103  46226  fourierdlem104  46227  fourierdlem109  46232  fourierdlem111  46234  fourierswlem  46247  fouriersw  46248  elaa2lem  46250  etransclem23  46274  etransclem24  46275  etransclem28  46279  etransclem38  46289  smfmullem1  46808  m1modmmod  47368  fargshiftfo  47452  lighneallem3  47617  nnsum4primeseven  47810  nnsum4primesevenALTV  47811  bgoldbtbndlem4  47818  bgoldbtbnd  47819  gpgedgvtx1  48072  dignn0flhalflem1  48626  affineid  48715  eenglngeehlnmlem1  48748  itsclquadb  48787