Theorem pncand 11670

Description: Cancellation law for subtraction. (Contributed by Mario Carneiro, 27-May-2016.)

Hypotheses

Ref	Expression
negidd.1	⊢ (𝜑 → 𝐴 ∈ ℂ)
pncand.2	⊢ (𝜑 → 𝐵 ∈ ℂ)

Assertion

Ref	Expression
pncand	⊢ (𝜑 → ((𝐴 + 𝐵) − 𝐵) = 𝐴)

Proof of Theorem pncand

Step	Hyp	Ref	Expression
1		negidd.1	. 2 ⊢ (𝜑 → 𝐴 ∈ ℂ)
2		pncand.2	. 2 ⊢ (𝜑 → 𝐵 ∈ ℂ)
3		pncan 11563	. 2 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((𝐴 + 𝐵) − 𝐵) = 𝐴)
4	1, 2, 3	syl2anc 596	1 ⊢ (𝜑 → ((𝐴 + 𝐵) − 𝐵) = 𝐴)

This proof depends on syntax axioms:   → wi 4   = wceq 1570   ∈ wcel 2145  (class class class)co 7420  ℂcc 11198   + caddc 11203   − cmin 11541

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 2213  ax-ext 2733  ax-sep 5249  ax-nul 5260  ax-pow 5327  ax-pr 5391  ax-un 7751  ax-resscn 11257  ax-1cn 11258  ax-icn 11259  ax-addcl 11260  ax-addrcl 11261  ax-mulcl 11262  ax-mulrcl 11263  ax-mulcom 11264  ax-addass 11265  ax-mulass 11266  ax-distr 11267  ax-i2m1 11268  ax-1ne0 11269  ax-1rid 11270  ax-rnegex 11271  ax-rrecex 11272  ax-cnre 11273  ax-pre-lttri 11274  ax-pre-lttrn 11275  ax-pre-ltadd 11276

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 2565  df-eu 2595  df-clab 2740  df-cleq 2753  df-clel 2836  df-nfc 2910  df-ne 2957  df-nel 3063  df-ral 3078  df-rex 3088  df-reu 3367  df-rab 3414  df-v 3453  df-sbc 3740  df-csb 3848  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-nul 4280  df-if 4483  df-pw 4559  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4868  df-br 5104  df-opab 5168  df-mpt 5187  df-id 5546  df-po 5559  df-so 5560  df-xp 5657  df-rel 5658  df-cnv 5659  df-co 5660  df-dm 5661  df-rn 5662  df-res 5663  df-ima 5664  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 8717  df-en 8974  df-dom 8975  df-sdom 8976  df-pnf 11345  df-mnf 11346  df-ltxr 11348  df-sub 11543

This theorem is used by:  mvlraddd  11724  mvlladdd  11725  mvrraddd  11727  mvrrsubd  11729  addlsub  11732  pnpncand  11737  pncan1  11740  eluzmn  12972  icoshftf1o  13605  xov1plusxeqvd  13629  fzom1ne1  13920  modaddb  14049  zesq  14370  hashdifsnp1  14651  ccatval3  14724  fsump1  15922  fsumrev2  15948  fprodp1  16136  risefacp1  16195  fallfacp1  16196  sadcp1  16625  smupp1  16650  hashdvds  16952  pythagtriplem4  16997  pythagtriplem6  16999  pythagtriplem7  17000  pythagtriplem12  17004  pythagtriplem14  17006  pcqdiv  17035  chnub  18796  chnlt  18797  chnccat  18800  mulgdirlem  19315  psdmplcl  22483  cayhamlem1  23184  pjthlem1  25758  ovolicopnf  25845  i1faddlem  26014  itg1addlem4  26020  itgpowd  26370  taylthlem2  26701  ulmshft  26717  efif1olem2  26871  efif1olem4  26873  logdiflbnd  27322  lgamgulmlem2  27357  lgamcvg2  27382  relgamcl  27389  ftalem2  27401  mulog2sumlem1  27861  mulog2sumlem3  27863  pntrlog2bndlem2  27905  pntrlog2bndlem4  27907  pntrlog2bndlem5  27908  colinearalglem4  29487  axpaschlem  29518  wwlksnred  30481  wwlksnext  30482  wwlksnredwwlkn  30484  wwlksnextproplem2  30499  clwlkclwwlklem2  30591  clwlkclwwlklem3  30592  clwwlkf  30638  wwlksext2clwwlk  30648  eucrct2eupth  30846  numclwwlk2lem1  30977  numclwlk2lem2f  30978  pjhthlem1  31993  fzm1ne1  33380  wrdt2ind  33516  cshwrnid  33522  psgnfzto1stlem  33661  cycpmco2lem4  33690  cycpmco2lem5  33691  cycpmco2lem7  33693  esplyindfv  34208  constraddcl  34394  constrremulcl  34399  madjusmdetlem2  34460  dya2icoseg  34909  fibp1  35033  ballotlemfc0  35125  ballotlemfcc  35126  ballotlemsgt1  35143  ballotlemsel1i  35145  ballotlemsima  35148  ballotlem1ri  35167  signstfvn  35198  reprsuc  35244  bcprod  36503  bccolsum  36504  unblimceq0  37373  knoppndvlem6  37383  bj-bary1lem1  38232  sin2h  38533  itg2addnclem  38589  itg2addnclem3  38591  areacirclem4  38629  ssbnd  38722  lcmineqlem10  43088  lcmineqlem11  43089  lcmineqlem18  43096  lcmineqlem19  43097  sticksstones12a  43207  sticksstones12  43208  aks6d1c6lem3  43222  bcle2d  43229  aks6d1c7lem1  43230  fz1sump1  43367  oddnumth  43368  dffltz  43670  jm2.19lem4  43998  jm2.23  44002  int-eqmvtd  45188  hashnzfzclim  45305  dvradcnv2  45330  binomcxplemnn0  45332  binomcxplemnotnn0  45339  nnsplit  46369  iccshift  46529  iooshift  46533  climinf  46617  limcperiod  46639  0ellimcdiv  46658  cncfshift  46883  cncfperiod  46888  dvdsn1add  46948  dvnmul  46952  itgiccshift  46989  itgperiod  46990  stoweidlem17  47026  wallispilem4  47077  wallispilem5  47078  stirlinglem1  47083  stirlinglem5  47087  stirlinglem6  47088  stirlinglem10  47092  dirkertrigeqlem2  47108  fourierdlem14  47130  fourierdlem19  47135  fourierdlem41  47157  fourierdlem42  47158  fourierdlem48  47163  fourierdlem49  47164  fourierdlem50  47165  fourierdlem64  47179  fourierdlem74  47189  fourierdlem75  47190  fourierdlem81  47196  fourierdlem92  47207  fourierdlem97  47212  fourierdlem103  47218  fourierdlem104  47219  fourierdlem107  47222  etransclem9  47252  nnfoctbdjlem  47464  chnerlem2  47892  fldivmod  48413  gpgvtxedg1  49161