Theorem npcand 11645

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

Hypotheses

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

Assertion

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

Proof of Theorem npcand

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

This proof depends on syntax axioms:   → wi 4   = wceq 1570   ∈ wcel 2145  (class class class)co 7408  ℂcc 11170   + caddc 11175   − cmin 11513

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 2732  ax-sep 5248  ax-nul 5259  ax-pow 5326  ax-pr 5390  ax-un 7734  ax-resscn 11229  ax-1cn 11230  ax-icn 11231  ax-addcl 11232  ax-addrcl 11233  ax-mulcl 11234  ax-mulrcl 11235  ax-mulcom 11236  ax-addass 11237  ax-mulass 11238  ax-distr 11239  ax-i2m1 11240  ax-1ne0 11241  ax-1rid 11242  ax-rnegex 11243  ax-rrecex 11244  ax-cnre 11245  ax-pre-lttri 11246  ax-pre-lttrn 11247  ax-pre-ltadd 11248

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 2564  df-eu 2594  df-clab 2739  df-cleq 2752  df-clel 2835  df-nfc 2909  df-ne 2956  df-nel 3062  df-ral 3077  df-rex 3087  df-reu 3366  df-rab 3413  df-v 3452  df-sbc 3739  df-csb 3847  df-dif 3901  df-un 3903  df-in 3905  df-ss 3915  df-nul 4279  df-if 4482  df-pw 4558  df-sn 4584  df-pr 4586  df-op 4590  df-uni 4867  df-br 5103  df-opab 5167  df-mpt 5186  df-id 5542  df-po 5555  df-so 5556  df-xp 5653  df-rel 5654  df-cnv 5655  df-co 5656  df-dm 5657  df-rn 5658  df-res 5659  df-ima 5660  df-iota 6483  df-fun 6529  df-fn 6530  df-f 6531  df-f1 6532  df-fo 6533  df-f1o 6534  df-fv 6535  df-riota 7365  df-ov 7411  df-oprab 7412  df-mpo 7413  df-er 8695  df-en 8952  df-dom 8953  df-sdom 8954  df-pnf 11317  df-mnf 11318  df-ltxr 11320  df-sub 11515

This theorem is used by:  addlsub  11702  npcan1  11711  ltsubadd  11756  lesubadd  11758  lesub1  11780  lincmb01cmp  13596  expaddzlem  14217  bcpasc  14433  bcn2m1  14436  swrdrn3  14770  cshwidxmod  14922  repswcshw  14931  swrds2m  15060  shftuz  15190  o1dif  15765  arisum2  15998  ntrivcvg  16034  ntrivcvgtail  16037  prodrblem  16064  fprodser  16084  fprodm1  16102  risefacval2  16145  fallfacval2  16146  fallfacfwd  16170  binomfallfaclem2  16174  sin01bnd  16321  moddvds  16401  dvdsexp  16466  bitscmp  16576  hashdvds  16914  vdwlem5  17125  vdwlem6  17126  vdwlem8  17128  chnrev  18763  omndmul3  20310  srgbinomlem4  20417  freshmansdream  21842  psdmul  22449  uniioombllem3  25868  i1faddlem  25976  itg1addlem4  25982  dvcnp2  26202  ftc1lem4  26321  dgrcolem2  26555  plydivlem4  26581  aaliou3lem8  26636  dvtaylp  26661  dvntaylp0  26663  taylthlem1  26664  efif1olem4  26837  tanarg  26911  quart1  27148  dmgmaddnn0  27318  lgamgulm2  27327  gamfac  27358  basellem9  27380  chtublem  27502  logexprlim  27516  dchrptlem1  27555  lgsquadlem1  27671  mudivsum  27821  logsqvma  27833  log2sumbnd  27835  selberglem2  27837  pntrlog2bndlem5  27872  pntlem3  27900  ostth2lem2  27925  brbtwn2  29417  cusgrsize2inds  29968  revwlk  30201  clwlkclwwlklem2  30525  clwwisshclwws  30540  clwwlkel  30571  clwwlkf  30572  clwwlknonex2lem1  30632  2clwwlk2clwwlk  30885  numclwwlk2  30916  fzspl  33315  fzsplit3  33319  bcm1n  33321  oexpled  33361  wrdt2ind  33450  psgnfzto1stlem  33595  cycpmco2lem5  33625  cycpmco2lem6  33626  esplyfvn  34143  vietalem  34145  ballotlemfc0  35060  ballotlemfcc  35061  signstfvn  35133  reprsuc  35179  breprexplemc  35196  lpadlen2  35248  bcm1nt  36423  itg2addnclem  38509  ftc1cnnclem  38529  ftc1anc  38539  caushft  38615  fzsplitnd  42952  lcmfunnnd  42982  lcmineqlem4  43002  lcmineqlem23  43021  intlewftc  43031  dvle2  43042  primrootsunit1  43067  aks6d1c5lem3  43107  aks6d1c5lem2  43108  sticksstones10  43125  sticksstones12a  43127  sticksstones16  43132  unitscyglem5  43169  nicomachus  43291  fltnltalem  43612  pellexlem6  43779  rmspecfund  43854  rmyluc  43882  jm2.18  43933  jm2.25  43944  hbtlem4  44071  bccm1k  45270  binomcxplemwb  45276  binomcxplemnotnn0  45284  oddfl  46215  zltlesub  46222  fzisoeu  46237  fperiodmul  46241  fzdifsuc2  46247  iccshift  46452  iooshift  46456  fmul01lt1lem2  46519  limcperiod  46562  sumnnodd  46564  cncfperiod  46811  fperdvper  46851  dvbdfbdioolem2  46861  dvnmul  46875  itgsinexp  46887  itgperiod  46913  stoweidlem11  46943  stoweidlem14  46946  stoweidlem26  46958  stoweidlem34  46966  wallispilem5  47001  stirlinglem5  47010  stirlinglem11  47016  stirlinglem12  47017  dirkercncflem1  47035  fourierdlem11  47050  fourierdlem15  47054  fourierdlem26  47065  fourierdlem41  47080  fourierdlem42  47081  fourierdlem48  47086  fourierdlem49  47087  fourierdlem63  47101  fourierdlem64  47102  fourierdlem65  47103  fourierdlem74  47112  fourierdlem75  47113  fourierdlem79  47117  fourierdlem81  47119  fourierdlem84  47122  fourierdlem88  47126  fourierdlem90  47128  fourierdlem92  47130  fourierdlem95  47133  fourierdlem97  47135  fourierdlem103  47141  fourierdlem104  47142  fourierdlem109  47147  fourierdlem111  47149  fourierswlem  47162  fouriersw  47163  elaa2lem  47165  etransclem23  47189  etransclem24  47190  etransclem28  47194  etransclem38  47204  smfmullem1  47723  m1modmmod  48356  fargshiftfo  48446  lighneallem3  48614  nnsum4primeseven  48820  nnsum4primesevenALTV  48821  bgoldbtbndlem4  48828  bgoldbtbnd  48829  gpgedgvtx1  49082  dignn0flhalflem1  49649  affineid  49738  eenglngeehlnmlem1  49771  itsclquadb  49810