Theorem pncand 10721

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

Syntax hints:   → wi 4   = wceq 1656   ∈ wcel 2164  (class class class)co 6910  ℂcc 10257   + caddc 10262   − cmin 10592

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1894  ax-4 1908  ax-5 2009  ax-6 2075  ax-7 2112  ax-8 2166  ax-9 2173  ax-10 2192  ax-11 2207  ax-12 2220  ax-13 2389  ax-ext 2803  ax-sep 5007  ax-nul 5015  ax-pow 5067  ax-pr 5129  ax-un 7214  ax-resscn 10316  ax-1cn 10317  ax-icn 10318  ax-addcl 10319  ax-addrcl 10320  ax-mulcl 10321  ax-mulrcl 10322  ax-mulcom 10323  ax-addass 10324  ax-mulass 10325  ax-distr 10326  ax-i2m1 10327  ax-1ne0 10328  ax-1rid 10329  ax-rnegex 10330  ax-rrecex 10331  ax-cnre 10332  ax-pre-lttri 10333  ax-pre-lttrn 10334  ax-pre-ltadd 10335

This theorem depends on definitions:  df-bi 199  df-an 387  df-or 879  df-3or 1112  df-3an 1113  df-tru 1660  df-ex 1879  df-nf 1883  df-sb 2068  df-mo 2605  df-eu 2640  df-clab 2812  df-cleq 2818  df-clel 2821  df-nfc 2958  df-ne 3000  df-nel 3103  df-ral 3122  df-rex 3123  df-reu 3124  df-rab 3126  df-v 3416  df-sbc 3663  df-csb 3758  df-dif 3801  df-un 3803  df-in 3805  df-ss 3812  df-nul 4147  df-if 4309  df-pw 4382  df-sn 4400  df-pr 4402  df-op 4406  df-uni 4661  df-br 4876  df-opab 4938  df-mpt 4955  df-id 5252  df-po 5265  df-so 5266  df-xp 5352  df-rel 5353  df-cnv 5354  df-co 5355  df-dm 5356  df-rn 5357  df-res 5358  df-ima 5359  df-iota 6090  df-fun 6129  df-fn 6130  df-f 6131  df-f1 6132  df-fo 6133  df-f1o 6134  df-fv 6135  df-riota 6871  df-ov 6913  df-oprab 6914  df-mpt2 6915  df-er 8014  df-en 8229  df-dom 8230  df-sdom 8231  df-pnf 10400  df-mnf 10401  df-ltxr 10403  df-sub 10594

This theorem is referenced by:  mvlraddd  10772  mvrraddd  10773  mvrladdd  10774  addlsub  10777  pnpncand  10782  pncan1  10785  eluzmn  11982  icoshftf1o  12593  xov1plusxeqvd  12618  zesq  13288  hashdifsnp1  13574  ccatval3  13646  fsumrev2  14895  binom1dif  14946  fprodp1  15079  risefacp1  15139  fallfacp1  15140  bpolydiflem  15164  sadcp1  15557  smupp1  15582  hashdvds  15858  pythagtriplem4  15902  pythagtriplem6  15904  pythagtriplem7  15905  pythagtriplem12  15909  pythagtriplem14  15911  pcqdiv  15940  mulgdirlem  17931  cayhamlem1  21048  blhalf  22587  pjthlem1  23612  ovolicopnf  23697  i1faddlem  23866  itg1addlem4  23872  aaliou3lem8  24506  taylthlem2  24534  ulmshft  24550  efif1olem2  24696  efif1olem4  24698  asinsin  25039  logdiflbnd  25141  harmonicbnd4  25157  lgamgulmlem2  25176  lgamcvg2  25201  relgamcl  25208  ftalem1  25219  ftalem2  25220  bcp1ctr  25424  2sqblem  25576  mulog2sumlem1  25643  mulog2sumlem3  25645  pntrlog2bndlem2  25687  pntrlog2bndlem4  25689  pntrlog2bndlem5  25690  pntrlog2bndlem6  25692  colinearalglem4  26215  axpaschlem  26246  wwlksnred  27209  wwlksnredOLD  27210  wwlksnredwwlkn  27214  wwlksnredwwlknOLD  27215  wwlksnextproplem2  27241  wwlksnextproplem2OLD  27242  clwlkclwwlklem2  27336  clwlkclwwlklem3  27337  clwwlkfOLD  27393  clwwlkf  27398  wwlksext2clwwlk  27409  eucrct2eupthOLD  27619  eucrct2eupth  27620  numclwwlk2lem1  27775  numclwlk2lem2f  27776  numclwlk2lem2fOLD  27779  numclwwlk2lem1OLD  27786  numclwlk2lem2fOLDOLD  27787  pjhthlem1  28801  psgnfzto1stlem  30391  madjusmdetlem2  30435  dya2icoseg  30880  iwrdsplitOLD  30991  fibp1  31005  ballotlemfc0  31096  ballotlemfcc  31097  ballotlemsgt1  31114  ballotlemsel1i  31116  ballotlemsima  31119  ballotlem1ri  31138  signstfvn  31189  reprsuc  31238  bcprod  32162  bccolsum  32163  unblimceq0  33025  knoppndvlem6  33035  bj-bary1lem1  33708  sin2h  33941  itg2addnclem  34003  itg2addnclem3  34005  areacirclem4  34045  ssbnd  34128  dffltz  38096  jm2.19lem4  38401  jm2.23  38405  itgpowd  38641  int-eqmvtd  39331  hashnzfzclim  39360  dvradcnv2  39385  binomcxplemnn0  39387  binomcxplemnotnn0  39394  nnsplit  40369  iccshift  40538  iooshift  40542  climinf  40631  limcperiod  40653  0ellimcdiv  40674  cncfshift  40880  cncfperiod  40885  dvdsn1add  40947  dvnmul  40951  dvnprodlem1  40954  itgiccshift  40988  itgperiod  40989  stoweidlem17  41026  wallispilem4  41077  wallispilem5  41078  stirlinglem1  41083  stirlinglem5  41087  stirlinglem6  41088  stirlinglem10  41092  dirkertrigeqlem2  41108  fourierdlem14  41130  fourierdlem19  41135  fourierdlem41  41157  fourierdlem42  41158  fourierdlem48  41163  fourierdlem49  41164  fourierdlem50  41165  fourierdlem64  41179  fourierdlem74  41189  fourierdlem75  41190  fourierdlem81  41196  fourierdlem92  41207  fourierdlem97  41212  fourierdlem103  41218  fourierdlem104  41219  fourierdlem107  41222  etransclem9  41252  nnfoctbdjlem  41461  fldivmod  43178  mvlladdd  43425