Theorem pncand 11598

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

This proof depends on syntax axioms:   → wi 4   = wceq 1570   ∈ wcel 2145  (class class class)co 7417  ℂcc 11126   + caddc 11131   − cmin 11469

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 7740  ax-resscn 11185  ax-1cn 11186  ax-icn 11187  ax-addcl 11188  ax-addrcl 11189  ax-mulcl 11190  ax-mulrcl 11191  ax-mulcom 11192  ax-addass 11193  ax-mulass 11194  ax-distr 11195  ax-i2m1 11196  ax-1ne0 11197  ax-1rid 11198  ax-rnegex 11199  ax-rrecex 11200  ax-cnre 11201  ax-pre-lttri 11202  ax-pre-lttrn 11203  ax-pre-ltadd 11204

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 7374  df-ov 7420  df-oprab 7421  df-mpo 7422  df-er 8700  df-en 8957  df-dom 8958  df-sdom 8959  df-pnf 11273  df-mnf 11274  df-ltxr 11276  df-sub 11471

This theorem is used by:  mvlraddd  11652  mvlladdd  11653  mvrraddd  11654  addlsub  11658  pnpncand  11663  pncan1  11666  eluzmn  12898  icoshftf1o  13531  xov1plusxeqvd  13555  fzom1ne1  13845  modaddb  13974  zesq  14294  hashdifsnp1  14575  ccatval3  14648  fsump1  15846  fsumrev2  15872  fprodp1  16062  risefacp1  16121  fallfacp1  16122  sadcp1  16551  smupp1  16576  hashdvds  16872  pythagtriplem4  16917  pythagtriplem6  16919  pythagtriplem7  16920  pythagtriplem12  16924  pythagtriplem14  16926  pcqdiv  16955  chnub  18716  chnlt  18717  chnccat  18720  mulgdirlem  19234  psdmplcl  22396  cayhamlem1  23097  pjthlem1  25671  ovolicopnf  25758  i1faddlem  25927  itg1addlem4  25933  itgpowd  26284  taylthlem2  26617  ulmshft  26633  efif1olem2  26788  efif1olem4  26790  logdiflbnd  27239  lgamgulmlem2  27274  lgamcvg2  27299  relgamcl  27306  ftalem2  27318  mulog2sumlem1  27778  mulog2sumlem3  27780  pntrlog2bndlem2  27822  pntrlog2bndlem4  27824  pntrlog2bndlem5  27825  colinearalglem4  29374  axpaschlem  29405  wwlksnred  30368  wwlksnext  30369  wwlksnredwwlkn  30371  wwlksnextproplem2  30386  clwlkclwwlklem2  30478  clwlkclwwlklem3  30479  clwwlkf  30525  wwlksext2clwwlk  30535  eucrct2eupth  30733  numclwwlk2lem1  30864  numclwlk2lem2f  30865  pjhthlem1  31880  fzm1ne1  33267  wrdt2ind  33403  cshwrnid  33409  psgnfzto1stlem  33548  cycpmco2lem4  33577  cycpmco2lem5  33578  cycpmco2lem7  33580  esplyindfv  34094  constraddcl  34280  constrremulcl  34285  madjusmdetlem2  34346  dya2icoseg  34796  fibp1  34920  ballotlemfc0  35012  ballotlemfcc  35013  ballotlemsgt1  35030  ballotlemsel1i  35032  ballotlemsima  35035  ballotlem1ri  35054  signstfvn  35085  reprsuc  35131  bcprod  36325  bccolsum  36326  unblimceq0  37212  knoppndvlem6  37222  bj-bary1lem1  38071  sin2h  38372  itg2addnclem  38428  itg2addnclem3  38430  areacirclem4  38468  ssbnd  38546  lcmineqlem10  42912  lcmineqlem11  42913  lcmineqlem18  42920  lcmineqlem19  42921  sticksstones12a  43031  sticksstones12  43032  aks6d1c6lem3  43046  bcle2d  43053  aks6d1c7lem1  43054  mvrrsubd  43157  fz1sump1  43193  oddnumth  43194  dffltz  43488  jm2.19lem4  43841  jm2.23  43845  int-eqmvtd  45037  hashnzfzclim  45154  dvradcnv2  45179  binomcxplemnn0  45181  binomcxplemnotnn0  45188  nnsplit  46196  iccshift  46356  iooshift  46360  climinf  46444  limcperiod  46466  0ellimcdiv  46485  cncfshift  46710  cncfperiod  46715  dvdsn1add  46775  dvnmul  46779  itgiccshift  46816  itgperiod  46817  stoweidlem17  46853  wallispilem4  46904  wallispilem5  46905  stirlinglem1  46910  stirlinglem5  46914  stirlinglem6  46915  stirlinglem10  46919  dirkertrigeqlem2  46935  fourierdlem14  46957  fourierdlem19  46962  fourierdlem41  46984  fourierdlem42  46985  fourierdlem48  46990  fourierdlem49  46991  fourierdlem50  46992  fourierdlem64  47006  fourierdlem74  47016  fourierdlem75  47017  fourierdlem81  47023  fourierdlem92  47034  fourierdlem97  47039  fourierdlem103  47045  fourierdlem104  47046  fourierdlem107  47049  etransclem9  47079  nnfoctbdjlem  47291  chnerlem2  47719  fldivmod  48240  gpgvtxedg1  48988