Theorem pncand 11480

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

Syntax hints:   → wi 4   = wceq 1541   ∈ wcel 2113  (class class class)co 7352  ℂcc 11011   + caddc 11016   − cmin 11351

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 2115  ax-9 2123  ax-10 2146  ax-11 2162  ax-12 2182  ax-ext 2705  ax-sep 5236  ax-nul 5246  ax-pow 5305  ax-pr 5372  ax-un 7674  ax-resscn 11070  ax-1cn 11071  ax-icn 11072  ax-addcl 11073  ax-addrcl 11074  ax-mulcl 11075  ax-mulrcl 11076  ax-mulcom 11077  ax-addass 11078  ax-mulass 11079  ax-distr 11080  ax-i2m1 11081  ax-1ne0 11082  ax-1rid 11083  ax-rnegex 11084  ax-rrecex 11085  ax-cnre 11086  ax-pre-lttri 11087  ax-pre-lttrn 11088  ax-pre-ltadd 11089

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 2068  df-mo 2537  df-eu 2566  df-clab 2712  df-cleq 2725  df-clel 2808  df-nfc 2882  df-ne 2930  df-nel 3034  df-ral 3049  df-rex 3058  df-reu 3348  df-rab 3397  df-v 3439  df-sbc 3738  df-csb 3847  df-dif 3901  df-un 3903  df-in 3905  df-ss 3915  df-nul 4283  df-if 4475  df-pw 4551  df-sn 4576  df-pr 4578  df-op 4582  df-uni 4859  df-br 5094  df-opab 5156  df-mpt 5175  df-id 5514  df-po 5527  df-so 5528  df-xp 5625  df-rel 5626  df-cnv 5627  df-co 5628  df-dm 5629  df-rn 5630  df-res 5631  df-ima 5632  df-iota 6442  df-fun 6488  df-fn 6489  df-f 6490  df-f1 6491  df-fo 6492  df-f1o 6493  df-fv 6494  df-riota 7309  df-ov 7355  df-oprab 7356  df-mpo 7357  df-er 8628  df-en 8876  df-dom 8877  df-sdom 8878  df-pnf 11155  df-mnf 11156  df-ltxr 11158  df-sub 11353

This theorem is referenced by:  mvlraddd  11534  mvlladdd  11535  mvrraddd  11536  addlsub  11540  pnpncand  11545  pncan1  11548  eluzmn  12745  icoshftf1o  13376  xov1plusxeqvd  13400  fzom1ne1  13687  modaddb  13815  zesq  14135  hashdifsnp1  14415  ccatval3  14488  fsump1  15665  fsumrev2  15691  fprodp1  15878  risefacp1  15938  fallfacp1  15939  sadcp1  16368  smupp1  16393  hashdvds  16688  pythagtriplem4  16733  pythagtriplem6  16735  pythagtriplem7  16736  pythagtriplem12  16740  pythagtriplem14  16742  pcqdiv  16771  chnub  18530  chnlt  18531  chnccat  18534  mulgdirlem  19020  psdmplcl  22078  cayhamlem1  22782  pjthlem1  25365  ovolicopnf  25453  i1faddlem  25622  itg1addlem4  25628  itgpowd  25985  taylthlem2  26310  taylthlem2OLD  26311  ulmshft  26327  efif1olem2  26480  efif1olem4  26482  logdiflbnd  26933  lgamgulmlem2  26968  lgamcvg2  26993  relgamcl  27000  ftalem2  27012  mulog2sumlem1  27473  mulog2sumlem3  27475  pntrlog2bndlem2  27517  pntrlog2bndlem4  27519  pntrlog2bndlem5  27520  colinearalglem4  28889  axpaschlem  28920  wwlksnred  29872  wwlksnext  29873  wwlksnredwwlkn  29875  wwlksnextproplem2  29890  clwlkclwwlklem2  29982  clwlkclwwlklem3  29983  clwwlkf  30029  wwlksext2clwwlk  30039  eucrct2eupth  30227  numclwwlk2lem1  30358  numclwlk2lem2f  30359  pjhthlem1  31373  fzm1ne1  32775  wrdt2ind  32941  cshwrnid  32949  psgnfzto1stlem  33076  cycpmco2lem4  33105  cycpmco2lem5  33106  cycpmco2lem7  33108  constraddcl  33796  constrremulcl  33801  madjusmdetlem2  33862  dya2icoseg  34311  fibp1  34435  ballotlemfc0  34527  ballotlemfcc  34528  ballotlemsgt1  34545  ballotlemsel1i  34547  ballotlemsima  34550  ballotlem1ri  34569  signstfvn  34603  reprsuc  34649  bcprod  35803  bccolsum  35804  unblimceq0  36572  knoppndvlem6  36582  bj-bary1lem1  37376  sin2h  37670  itg2addnclem  37731  itg2addnclem3  37733  areacirclem4  37771  ssbnd  37848  lcmineqlem10  42151  lcmineqlem11  42152  lcmineqlem18  42159  lcmineqlem19  42160  sticksstones12a  42270  sticksstones12  42271  aks6d1c6lem3  42285  bcle2d  42292  aks6d1c7lem1  42293  mvrrsubd  42392  fz1sump1  42428  oddnumth  42429  dffltz  42752  jm2.19lem4  43109  jm2.23  43113  int-eqmvtd  44306  hashnzfzclim  44439  dvradcnv2  44464  binomcxplemnn0  44466  binomcxplemnotnn0  44473  nnsplit  45481  iccshift  45642  iooshift  45646  climinf  45730  limcperiod  45752  0ellimcdiv  45771  cncfshift  45996  cncfperiod  46001  dvdsn1add  46061  dvnmul  46065  itgiccshift  46102  itgperiod  46103  stoweidlem17  46139  wallispilem4  46190  wallispilem5  46191  stirlinglem1  46196  stirlinglem5  46200  stirlinglem6  46201  stirlinglem10  46205  dirkertrigeqlem2  46221  fourierdlem14  46243  fourierdlem19  46248  fourierdlem41  46270  fourierdlem42  46271  fourierdlem48  46276  fourierdlem49  46277  fourierdlem50  46278  fourierdlem64  46292  fourierdlem74  46302  fourierdlem75  46303  fourierdlem81  46309  fourierdlem92  46320  fourierdlem97  46325  fourierdlem103  46331  fourierdlem104  46332  fourierdlem107  46335  etransclem9  46365  nnfoctbdjlem  46577  chnerlem2  47005  fldivmod  47462  gpgvtxedg1  48188