Theorem pncan 11463

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

Assertion

Ref	Expression
pncan	⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((𝐴 + 𝐵) − 𝐵) = 𝐴)

Proof of Theorem pncan

Step	Hyp	Ref	Expression
1		simpr 486	. . 3 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → 𝐵 ∈ ℂ)
2		simpl 484	. . 3 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → 𝐴 ∈ ℂ)
3	1, 2	addcomd 11413	. 2 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐵 + 𝐴) = (𝐴 + 𝐵))
4		addcl 11189	. . 3 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 + 𝐵) ∈ ℂ)
5		subadd 11460	. . 3 ⊢ (((𝐴 + 𝐵) ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐴 ∈ ℂ) → (((𝐴 + 𝐵) − 𝐵) = 𝐴 ↔ (𝐵 + 𝐴) = (𝐴 + 𝐵)))
6	4, 1, 2, 5	syl3anc 1372	. 2 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (((𝐴 + 𝐵) − 𝐵) = 𝐴 ↔ (𝐵 + 𝐴) = (𝐴 + 𝐵)))
7	3, 6	mpbird 257	1 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((𝐴 + 𝐵) − 𝐵) = 𝐴)

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 397   = wceq 1542   ∈ wcel 2107  (class class class)co 7406  ℂcc 11105   + caddc 11110   − cmin 11441

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2704  ax-sep 5299  ax-nul 5306  ax-pow 5363  ax-pr 5427  ax-un 7722  ax-resscn 11164  ax-1cn 11165  ax-icn 11166  ax-addcl 11167  ax-addrcl 11168  ax-mulcl 11169  ax-mulrcl 11170  ax-mulcom 11171  ax-addass 11172  ax-mulass 11173  ax-distr 11174  ax-i2m1 11175  ax-1ne0 11176  ax-1rid 11177  ax-rnegex 11178  ax-rrecex 11179  ax-cnre 11180  ax-pre-lttri 11181  ax-pre-lttrn 11182  ax-pre-ltadd 11183

This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3or 1089  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2535  df-eu 2564  df-clab 2711  df-cleq 2725  df-clel 2811  df-nfc 2886  df-ne 2942  df-nel 3048  df-ral 3063  df-rex 3072  df-reu 3378  df-rab 3434  df-v 3477  df-sbc 3778  df-csb 3894  df-dif 3951  df-un 3953  df-in 3955  df-ss 3965  df-nul 4323  df-if 4529  df-pw 4604  df-sn 4629  df-pr 4631  df-op 4635  df-uni 4909  df-br 5149  df-opab 5211  df-mpt 5232  df-id 5574  df-po 5588  df-so 5589  df-xp 5682  df-rel 5683  df-cnv 5684  df-co 5685  df-dm 5686  df-rn 5687  df-res 5688  df-ima 5689  df-iota 6493  df-fun 6543  df-fn 6544  df-f 6545  df-f1 6546  df-fo 6547  df-f1o 6548  df-fv 6549  df-riota 7362  df-ov 7409  df-oprab 7410  df-mpo 7411  df-er 8700  df-en 8937  df-dom 8938  df-sdom 8939  df-pnf 11247  df-mnf 11248  df-ltxr 11250  df-sub 11443

This theorem is referenced by:  pncan2  11464  addsubass  11467  pncan3oi  11473  subid1  11477  nppcan2  11488  pncand  11569  nn1m1nn  12230  nnsub  12253  elnn0nn  12511  elz2  12573  zrevaddcl  12604  nzadd  12607  qrevaddcl  12952  irradd  12954  fzrev3  13564  elfzp1b  13575  fzrevral3  13585  fzval3  13698  seqf1olem1  14004  seqf1olem2  14005  bcp1nk  14274  bcp1m1  14277  bcpasc  14278  hashbclem  14408  ccatalpha  14540  wrdind  14669  wrd2ind  14670  2cshwcshw  14773  shftlem  15012  shftval5  15022  isershft  15607  isercoll2  15612  mptfzshft  15721  telfsumo  15745  fsumparts  15749  bcxmas  15778  isum1p  15784  geolim  15813  mertenslem2  15828  mertens  15829  fsumkthpow  15997  eftlub  16049  effsumlt  16051  eirrlem  16144  dvdsadd  16242  prmind2  16619  iserodd  16765  fldivp1  16827  prmpwdvds  16834  pockthlem  16835  prmreclem4  16849  prmreclem6  16851  4sqlem11  16885  vdwapun  16904  ramub1lem1  16956  ramcl  16959  efgsval2  19596  efgsrel  19597  shft2rab  25017  uniioombllem3  25094  uniioombllem4  25095  dvexp  25462  dvfsumlem1  25535  degltp1le  25583  ply1divex  25646  plyaddlem1  25719  plymullem1  25720  dvply1  25789  dvply2g  25790  vieta1lem2  25816  aaliou3lem7  25854  dvradcnv  25925  pserdvlem2  25932  abssinper  26022  advlogexp  26155  atantayl3  26434  leibpilem2  26436  emcllem2  26491  harmonicbnd4  26505  basellem8  26582  ppiprm  26645  ppinprm  26646  chtprm  26647  chtnprm  26648  chpp1  26649  chtub  26705  perfectlem1  26722  perfectlem2  26723  perfect  26724  bcp1ctr  26772  lgsvalmod  26809  lgseisen  26872  lgsquadlem1  26873  lgsquad2lem1  26877  2sqlem10  26921  rplogsumlem1  26977  selberg2lem  27043  logdivbnd  27049  pntrsumo1  27058  pntpbnd2  27080  clwwlkf1  29292  subfacp1lem5  34164  subfacp1lem6  34165  subfacval2  34167  subfaclim  34168  cvmliftlem7  34271  cvmliftlem10  34274  mblfinlem2  36515  itg2addnclem3  36530  fdc  36602  mettrifi  36614  heiborlem4  36671  heiborlem6  36673  lzenom  41494  2nn0ind  41670  jm2.17a  41685  jm2.17b  41686  jm2.17c  41687  evensumeven  46362  perfectALTVlem2  46377  perfectALTV  46378