MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  pncand Structured version   Visualization version   GIF version

Theorem pncand 10378
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
StepHypRef Expression
1 negidd.1 . 2 (𝜑𝐴 ∈ ℂ)
2 pncand.2 . 2 (𝜑𝐵 ∈ ℂ)
3 pncan 10272 . 2 ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((𝐴 + 𝐵) − 𝐵) = 𝐴)
41, 2, 3syl2anc 692 1 (𝜑 → ((𝐴 + 𝐵) − 𝐵) = 𝐴)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1481  wcel 1988  (class class class)co 6635  cc 9919   + caddc 9924  cmin 10251
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1720  ax-4 1735  ax-5 1837  ax-6 1886  ax-7 1933  ax-8 1990  ax-9 1997  ax-10 2017  ax-11 2032  ax-12 2045  ax-13 2244  ax-ext 2600  ax-sep 4772  ax-nul 4780  ax-pow 4834  ax-pr 4897  ax-un 6934  ax-resscn 9978  ax-1cn 9979  ax-icn 9980  ax-addcl 9981  ax-addrcl 9982  ax-mulcl 9983  ax-mulrcl 9984  ax-mulcom 9985  ax-addass 9986  ax-mulass 9987  ax-distr 9988  ax-i2m1 9989  ax-1ne0 9990  ax-1rid 9991  ax-rnegex 9992  ax-rrecex 9993  ax-cnre 9994  ax-pre-lttri 9995  ax-pre-lttrn 9996  ax-pre-ltadd 9997
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3or 1037  df-3an 1038  df-tru 1484  df-ex 1703  df-nf 1708  df-sb 1879  df-eu 2472  df-mo 2473  df-clab 2607  df-cleq 2613  df-clel 2616  df-nfc 2751  df-ne 2792  df-nel 2895  df-ral 2914  df-rex 2915  df-reu 2916  df-rab 2918  df-v 3197  df-sbc 3430  df-csb 3527  df-dif 3570  df-un 3572  df-in 3574  df-ss 3581  df-nul 3908  df-if 4078  df-pw 4151  df-sn 4169  df-pr 4171  df-op 4175  df-uni 4428  df-br 4645  df-opab 4704  df-mpt 4721  df-id 5014  df-po 5025  df-so 5026  df-xp 5110  df-rel 5111  df-cnv 5112  df-co 5113  df-dm 5114  df-rn 5115  df-res 5116  df-ima 5117  df-iota 5839  df-fun 5878  df-fn 5879  df-f 5880  df-f1 5881  df-fo 5882  df-f1o 5883  df-fv 5884  df-riota 6596  df-ov 6638  df-oprab 6639  df-mpt2 6640  df-er 7727  df-en 7941  df-dom 7942  df-sdom 7943  df-pnf 10061  df-mnf 10062  df-ltxr 10064  df-sub 10253
This theorem is referenced by:  mvlraddd  10429  mvrraddd  10430  addlsub  10432  pnpncand  10437  pncan1  10439  eluzmn  11679  icoshftf1o  12280  xov1plusxeqvd  12303  zesq  12970  brfi1indlem  13261  ccatval3  13346  fsumrev2  14495  binom1dif  14546  fprodp1  14680  risefacp1  14741  fallfacp1  14742  bpolydiflem  14766  sadcp1  15158  smupp1  15183  hashdvds  15461  pythagtriplem4  15505  pythagtriplem6  15507  pythagtriplem7  15508  pythagtriplem12  15512  pythagtriplem14  15514  pcqdiv  15543  mulgdirlem  17553  cayhamlem1  20652  blhalf  22191  pjthlem1  23189  ovolicopnf  23273  i1faddlem  23441  itg1addlem4  23447  ftc1lem4  23783  aaliou3lem8  24081  taylthlem2  24109  ulmshft  24125  efif1olem2  24270  efif1olem4  24272  quart1lem  24563  asinsin  24600  efiatan2  24625  logdiflbnd  24702  harmonicbnd4  24718  lgamgulmlem2  24737  lgamcvg2  24762  relgamcl  24769  ftalem1  24780  ftalem2  24781  bcctr  24981  pcbcctr  24982  bcp1ctr  24985  2sqblem  25137  mulog2sumlem1  25204  mulog2sumlem3  25206  pntrlog2bndlem2  25248  pntrlog2bndlem4  25250  pntrlog2bndlem5  25251  pntrlog2bndlem6  25253  colinearalglem4  25770  axpaschlem  25801  wwlksnred  26768  wwlksnredwwlkn  26771  wwlksnextproplem2  26786  clwlkclwwlklem2  26882  clwlkclwwlklem3  26883  clwwlksf  26895  wwlksext2clwwlk  26904  eucrct2eupth  27085  numclwwlk2lem1  27206  numclwlk2lem2f  27207  pjhthlem1  28220  psgnfzto1stlem  29824  madjusmdetlem2  29868  dya2icoseg  30313  iwrdsplit  30423  fibp1  30437  ballotlemfc0  30528  ballotlemfcc  30529  ballotlemsgt1  30546  ballotlemsel1i  30548  ballotlemsima  30551  ballotlem1ri  30570  signstfvn  30620  reprsuc  30667  bcprod  31599  bccolsum  31600  unblimceq0  32473  knoppndvlem6  32483  bj-bary1lem1  33132  sin2h  33370  itg2addnclem  33432  itg2addnclem3  33434  ftc1cnnclem  33454  areacirclem4  33474  ssbnd  33558  jm2.19lem4  37378  jm2.23  37382  jm3.1lem1  37403  itgpowd  37619  int-eqmvtd  38312  hashnzfzclim  38341  dvradcnv2  38366  binomcxplemnn0  38368  binomcxplemnotnn0  38375  nnsplit  39387  iccshift  39547  iooshift  39551  climinf  39638  limcperiod  39660  0ellimcdiv  39681  cncfshift  39850  cncfperiod  39855  dvdsn1add  39917  dvnmul  39921  dvnprodlem1  39924  itgiccshift  39959  itgperiod  39960  stoweidlem17  39997  wallispilem4  40048  wallispilem5  40049  stirlinglem1  40054  stirlinglem5  40058  stirlinglem6  40059  stirlinglem10  40063  dirkertrigeqlem2  40079  fourierdlem14  40101  fourierdlem19  40106  fourierdlem41  40128  fourierdlem42  40129  fourierdlem48  40134  fourierdlem49  40135  fourierdlem50  40136  fourierdlem64  40150  fourierdlem74  40160  fourierdlem75  40161  fourierdlem81  40167  fourierdlem92  40178  fourierdlem97  40183  fourierdlem103  40189  fourierdlem104  40190  fourierdlem107  40193  etransclem9  40223  nnfoctbdjlem  40435  fldivmod  42078  mvlladdd  42278  mvrladdd  42280
  Copyright terms: Public domain W3C validator