Theorem pncand 11379

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

Syntax hints:   → wi 4   = wceq 1539   ∈ wcel 2104  (class class class)co 7307  ℂcc 10915   + caddc 10920   − cmin 11251

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1911  ax-6 1969  ax-7 2009  ax-8 2106  ax-9 2114  ax-10 2135  ax-11 2152  ax-12 2169  ax-ext 2707  ax-sep 5232  ax-nul 5239  ax-pow 5297  ax-pr 5361  ax-un 7620  ax-resscn 10974  ax-1cn 10975  ax-icn 10976  ax-addcl 10977  ax-addrcl 10978  ax-mulcl 10979  ax-mulrcl 10980  ax-mulcom 10981  ax-addass 10982  ax-mulass 10983  ax-distr 10984  ax-i2m1 10985  ax-1ne0 10986  ax-1rid 10987  ax-rnegex 10988  ax-rrecex 10989  ax-cnre 10990  ax-pre-lttri 10991  ax-pre-lttrn 10992  ax-pre-ltadd 10993

This theorem depends on definitions:  df-bi 206  df-an 398  df-or 846  df-3or 1088  df-3an 1089  df-tru 1542  df-fal 1552  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2538  df-eu 2567  df-clab 2714  df-cleq 2728  df-clel 2814  df-nfc 2887  df-ne 2942  df-nel 3048  df-ral 3063  df-rex 3072  df-reu 3286  df-rab 3287  df-v 3439  df-sbc 3722  df-csb 3838  df-dif 3895  df-un 3897  df-in 3899  df-ss 3909  df-nul 4263  df-if 4466  df-pw 4541  df-sn 4566  df-pr 4568  df-op 4572  df-uni 4845  df-br 5082  df-opab 5144  df-mpt 5165  df-id 5500  df-po 5514  df-so 5515  df-xp 5606  df-rel 5607  df-cnv 5608  df-co 5609  df-dm 5610  df-rn 5611  df-res 5612  df-ima 5613  df-iota 6410  df-fun 6460  df-fn 6461  df-f 6462  df-f1 6463  df-fo 6464  df-f1o 6465  df-fv 6466  df-riota 7264  df-ov 7310  df-oprab 7311  df-mpo 7312  df-er 8529  df-en 8765  df-dom 8766  df-sdom 8767  df-pnf 11057  df-mnf 11058  df-ltxr 11060  df-sub 11253

This theorem is referenced by:  mvlraddd  11431  mvlladdd  11432  mvrraddd  11433  addlsub  11437  pnpncand  11442  pncan1  11445  eluzmn  12635  icoshftf1o  13252  xov1plusxeqvd  13276  zesq  13987  hashdifsnp1  14255  ccatval3  14329  fsumrev2  15539  fprodp1  15724  risefacp1  15784  fallfacp1  15785  sadcp1  16207  smupp1  16232  hashdvds  16521  pythagtriplem4  16565  pythagtriplem6  16567  pythagtriplem7  16568  pythagtriplem12  16572  pythagtriplem14  16574  pcqdiv  16603  mulgdirlem  18779  cayhamlem1  22060  pjthlem1  24646  ovolicopnf  24733  i1faddlem  24902  itg1addlem4  24908  itg1addlem4OLD  24909  itgpowd  25259  taylthlem2  25578  ulmshft  25594  efif1olem2  25744  efif1olem4  25746  logdiflbnd  26189  lgamgulmlem2  26224  lgamcvg2  26249  relgamcl  26256  ftalem2  26268  mulog2sumlem1  26727  mulog2sumlem3  26729  pntrlog2bndlem2  26771  pntrlog2bndlem4  26773  pntrlog2bndlem5  26774  colinearalglem4  27322  axpaschlem  27353  wwlksnred  28302  wwlksnext  28303  wwlksnredwwlkn  28305  wwlksnextproplem2  28320  clwlkclwwlklem2  28409  clwlkclwwlklem3  28410  clwwlkf  28456  wwlksext2clwwlk  28466  eucrct2eupth  28654  numclwwlk2lem1  28785  numclwlk2lem2f  28786  pjhthlem1  29798  fzm1ne1  31155  fzom1ne1  31167  wrdt2ind  31270  cshwrnid  31278  psgnfzto1stlem  31412  cycpmco2lem4  31441  cycpmco2lem5  31442  cycpmco2lem7  31444  madjusmdetlem2  31823  dya2icoseg  32289  fibp1  32413  ballotlemfc0  32504  ballotlemfcc  32505  ballotlemsgt1  32522  ballotlemsel1i  32524  ballotlemsima  32527  ballotlem1ri  32546  signstfvn  32593  reprsuc  32640  bcprod  33749  bccolsum  33750  unblimceq0  34732  knoppndvlem6  34742  bj-bary1lem1  35526  sin2h  35811  itg2addnclem  35872  itg2addnclem3  35874  areacirclem4  35912  ssbnd  35990  lcmineqlem10  40088  lcmineqlem11  40089  lcmineqlem18  40096  lcmineqlem19  40097  sticksstones12a  40155  sticksstones12  40156  metakunt12  40178  mvrrsubd  40340  dffltz  40508  jm2.19lem4  40852  jm2.23  40856  int-eqmvtd  41838  hashnzfzclim  41978  dvradcnv2  42003  binomcxplemnn0  42005  binomcxplemnotnn0  42012  nnsplit  42945  iccshift  43105  iooshift  43109  climinf  43196  limcperiod  43218  0ellimcdiv  43239  cncfshift  43464  cncfperiod  43469  dvdsn1add  43529  dvnmul  43533  dvnprodlem1  43536  itgiccshift  43570  itgperiod  43571  stoweidlem17  43607  wallispilem4  43658  wallispilem5  43659  stirlinglem1  43664  stirlinglem5  43668  stirlinglem6  43669  stirlinglem10  43673  dirkertrigeqlem2  43689  fourierdlem14  43711  fourierdlem19  43716  fourierdlem41  43738  fourierdlem42  43739  fourierdlem48  43744  fourierdlem49  43745  fourierdlem50  43746  fourierdlem64  43760  fourierdlem74  43770  fourierdlem75  43771  fourierdlem81  43777  fourierdlem92  43788  fourierdlem97  43793  fourierdlem103  43799  fourierdlem104  43800  fourierdlem107  43803  etransclem9  43833  nnfoctbdjlem  44043  fldivmod  45922