Theorem npcand 11509

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

Syntax hints:   → wi 4   = wceq 1542   ∈ wcel 2114  (class class class)co 7367  ℂcc 11036   + caddc 11041   − cmin 11377

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2709  ax-sep 5232  ax-nul 5242  ax-pow 5308  ax-pr 5376  ax-un 7689  ax-resscn 11095  ax-1cn 11096  ax-icn 11097  ax-addcl 11098  ax-addrcl 11099  ax-mulcl 11100  ax-mulrcl 11101  ax-mulcom 11102  ax-addass 11103  ax-mulass 11104  ax-distr 11105  ax-i2m1 11106  ax-1ne0 11107  ax-1rid 11108  ax-rnegex 11109  ax-rrecex 11110  ax-cnre 11111  ax-pre-lttri 11112  ax-pre-lttrn 11113  ax-pre-ltadd 11114

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2540  df-eu 2570  df-clab 2716  df-cleq 2729  df-clel 2812  df-nfc 2886  df-ne 2934  df-nel 3038  df-ral 3053  df-rex 3063  df-reu 3344  df-rab 3391  df-v 3432  df-sbc 3730  df-csb 3839  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-nul 4275  df-if 4468  df-pw 4544  df-sn 4569  df-pr 4571  df-op 4575  df-uni 4852  df-br 5087  df-opab 5149  df-mpt 5168  df-id 5526  df-po 5539  df-so 5540  df-xp 5637  df-rel 5638  df-cnv 5639  df-co 5640  df-dm 5641  df-rn 5642  df-res 5643  df-ima 5644  df-iota 6455  df-fun 6501  df-fn 6502  df-f 6503  df-f1 6504  df-fo 6505  df-f1o 6506  df-fv 6507  df-riota 7324  df-ov 7370  df-oprab 7371  df-mpo 7372  df-er 8643  df-en 8894  df-dom 8895  df-sdom 8896  df-pnf 11181  df-mnf 11182  df-ltxr 11184  df-sub 11379

This theorem is referenced by:  addlsub  11566  npcan1  11575  ltsubadd  11620  lesubadd  11622  lesub1  11644  lincmb01cmp  13448  expaddzlem  14067  bcpasc  14283  bcn2m1  14286  cshwidxmod  14765  repswcshw  14774  swrds2m  14903  shftuz  15031  o1dif  15592  arisum2  15826  ntrivcvg  15862  ntrivcvgtail  15865  prodrblem  15894  fprodser  15914  fprodm1  15932  risefacval2  15975  fallfacval2  15976  fallfacfwd  16001  binomfallfaclem2  16005  sin01bnd  16152  moddvds  16232  dvdsexp  16297  bitscmp  16407  hashdvds  16745  vdwlem5  16956  vdwlem6  16957  vdwlem8  16959  chnrev  18593  omndmul3  20109  srgbinomlem4  20210  freshmansdream  21554  psdmul  22132  uniioombllem3  25552  i1faddlem  25660  itg1addlem4  25666  dvcnp2  25887  ftc1lem4  26006  dgrcolem2  26239  plydivlem4  26262  aaliou3lem8  26311  dvtaylp  26335  dvntaylp0  26337  taylthlem1  26338  efif1olem4  26509  tanarg  26583  quart1  26820  dmgmaddnn0  26990  lgamgulm2  26999  gamfac  27030  basellem9  27052  chtublem  27174  logexprlim  27188  dchrptlem1  27227  lgsquadlem1  27343  mudivsum  27493  logsqvma  27505  log2sumbnd  27507  selberglem2  27509  pntrlog2bndlem5  27544  pntlem3  27572  ostth2lem2  27597  brbtwn2  28974  cusgrsize2inds  29522  clwlkclwwlklem2  30070  clwwisshclwws  30085  clwwlkel  30116  clwwlkf  30117  clwwlknonex2lem1  30177  2clwwlk2clwwlk  30420  numclwwlk2  30451  fzspl  32862  fzsplit3  32866  bcm1n  32868  oexpled  32920  wrdt2ind  33013  swrdrn3  33015  psgnfzto1stlem  33161  cycpmco2lem5  33191  cycpmco2lem6  33192  esplyfvn  33721  vietalem  33723  ballotlemfc0  34637  ballotlemfcc  34638  signstfvn  34713  reprsuc  34759  breprexplemc  34776  lpadlen2  34825  revwlk  35307  bcm1nt  35919  itg2addnclem  37992  ftc1cnnclem  38012  ftc1anc  38022  caushft  38082  fzsplitnd  42421  lcmfunnnd  42451  lcmineqlem4  42471  lcmineqlem23  42490  intlewftc  42500  dvle2  42511  primrootsunit1  42536  aks6d1c5lem3  42576  aks6d1c5lem2  42577  sticksstones10  42594  sticksstones12a  42596  sticksstones16  42601  unitscyglem5  42638  nicomachus  42744  fltnltalem  43095  pellexlem6  43262  rmspecfund  43337  rmyluc  43365  jm2.18  43416  jm2.25  43427  hbtlem4  43554  bccm1k  44769  binomcxplemwb  44775  binomcxplemnotnn0  44783  oddfl  45711  zltlesub  45718  fzisoeu  45733  fperiodmul  45737  fzdifsuc2  45743  iccshift  45948  iooshift  45952  fmul01lt1lem2  46015  limcperiod  46058  sumnnodd  46060  cncfperiod  46307  fperdvper  46347  dvbdfbdioolem2  46357  dvnmul  46371  itgsinexp  46383  itgperiod  46409  stoweidlem11  46439  stoweidlem14  46442  stoweidlem26  46454  stoweidlem34  46462  wallispilem5  46497  stirlinglem5  46506  stirlinglem11  46512  stirlinglem12  46513  dirkercncflem1  46531  fourierdlem11  46546  fourierdlem15  46550  fourierdlem26  46561  fourierdlem41  46576  fourierdlem42  46577  fourierdlem48  46582  fourierdlem49  46583  fourierdlem63  46597  fourierdlem64  46598  fourierdlem65  46599  fourierdlem74  46608  fourierdlem75  46609  fourierdlem79  46613  fourierdlem81  46615  fourierdlem84  46618  fourierdlem88  46622  fourierdlem90  46624  fourierdlem92  46626  fourierdlem95  46629  fourierdlem97  46631  fourierdlem103  46637  fourierdlem104  46638  fourierdlem109  46643  fourierdlem111  46645  fourierswlem  46658  fouriersw  46659  elaa2lem  46661  etransclem23  46685  etransclem24  46686  etransclem28  46690  etransclem38  46700  smfmullem1  47219  m1modmmod  47806  fargshiftfo  47896  lighneallem3  48064  nnsum4primeseven  48270  nnsum4primesevenALTV  48271  bgoldbtbndlem4  48278  bgoldbtbnd  48279  gpgedgvtx1  48532  dignn0flhalflem1  49085  affineid  49174  eenglngeehlnmlem1  49207  itsclquadb  49246