Theorem pncan 11429

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 488	. . 3 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → 𝐵 ∈ ℂ)
2		simpl 486	. . 3 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → 𝐴 ∈ ℂ)
3	1, 2	addcomd 11378	. 2 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐵 + 𝐴) = (𝐴 + 𝐵))
4		addcl 11148	. . 3 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 + 𝐵) ∈ ℂ)
5		subadd 11426	. . 3 ⊢ (((𝐴 + 𝐵) ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐴 ∈ ℂ) → (((𝐴 + 𝐵) − 𝐵) = 𝐴 ↔ (𝐵 + 𝐴) = (𝐴 + 𝐵)))
6	4, 1, 2, 5	syl3anc 1389	. 2 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (((𝐴 + 𝐵) − 𝐵) = 𝐴 ↔ (𝐵 + 𝐴) = (𝐴 + 𝐵)))
7	3, 6	mpbird 259	1 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((𝐴 + 𝐵) − 𝐵) = 𝐴)

Syntax hints:   → wi 4   ↔ wb 208   ∧ wa 399   = wceq 1559   ∈ wcel 2141  (class class class)co 7390  ℂcc 11064   + caddc 11069   − cmin 11407

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-8 2143  ax-9 2151  ax-10 2174  ax-11 2190  ax-12 2211  ax-ext 2733  ax-sep 5243  ax-nul 5253  ax-pow 5319  ax-pr 5387  ax-un 7712  ax-resscn 11123  ax-1cn 11124  ax-icn 11125  ax-addcl 11126  ax-addrcl 11127  ax-mulcl 11128  ax-mulrcl 11129  ax-mulcom 11130  ax-addass 11131  ax-mulass 11132  ax-distr 11133  ax-i2m1 11134  ax-1ne0 11135  ax-1rid 11136  ax-rnegex 11137  ax-rrecex 11138  ax-cnre 11139  ax-pre-lttri 11140  ax-pre-lttrn 11141  ax-pre-ltadd 11142

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-3or 1098  df-3an 1099  df-tru 1562  df-fal 1572  df-ex 1799  df-nf 1803  df-sb 2090  df-mo 2565  df-eu 2595  df-clab 2740  df-cleq 2753  df-clel 2836  df-nfc 2910  df-ne 2957  df-nel 3061  df-ral 3076  df-rex 3086  df-reu 3367  df-rab 3414  df-v 3455  df-sbc 3743  df-csb 3851  df-dif 3905  df-un 3907  df-in 3909  df-ss 3919  df-nul 4284  df-if 4478  df-pw 4554  df-sn 4580  df-pr 4582  df-op 4586  df-uni 4863  df-br 5098  df-opab 5160  df-mpt 5179  df-id 5538  df-po 5551  df-so 5552  df-xp 5649  df-rel 5650  df-cnv 5651  df-co 5652  df-dm 5653  df-rn 5654  df-res 5655  df-ima 5656  df-iota 6471  df-fun 6517  df-fn 6518  df-f 6519  df-f1 6520  df-fo 6521  df-f1o 6522  df-fv 6523  df-riota 7347  df-ov 7393  df-oprab 7394  df-mpo 7395  df-er 8671  df-en 8921  df-dom 8922  df-sdom 8923  df-pnf 11211  df-mnf 11212  df-ltxr 11214  df-sub 11409

This theorem is referenced by:  pncan2  11430  addsubass  11433  pncan3oi  11439  subid1  11444  nppcan2  11455  pncand  11536  nn1m1nn  12224  nnsub  12250  elnn0nn  12516  elz2  12579  zrevaddcl  12609  nzadd  12612  qrevaddcl  12965  irradd  12967  fzrev3  13588  elfzp1b  13599  fzrevral3  13612  fzval3  13733  seqf1olem1  14047  seqf1olem2  14048  bcp1nk  14323  bcp1m1  14326  bcpasc  14327  hashbclem  14458  ccatalpha  14600  wrdind  14728  wrd2ind  14729  2cshwcshw  14831  shftlem  15074  shftval5  15084  isershft  15681  isercoll2  15686  mptfzshft  15795  telfsumo  15820  fsumparts  15824  bcxmas  15855  isum1p  15861  geolim  15890  mertenslem2  15905  mertens  15906  fsumkthpow  16076  eftlub  16131  effsumlt  16133  eirrlem  16226  dvdsadd  16326  prmind2  16709  iserodd  16861  fldivp1  16923  prmpwdvds  16930  pockthlem  16931  prmreclem4  16945  prmreclem6  16947  4sqlem11  16981  vdwapun  17000  ramub1lem1  17052  ramcl  17055  efgsval2  19763  efgsrel  19764  shft2rab  25557  uniioombllem3  25634  uniioombllem4  25635  dvexp  26002  dvfsumlem1  26075  degltp1le  26120  ply1divex  26184  plyaddlem1  26260  plymullem1  26261  dvply1  26335  dvply2g  26336  vieta1lem2  26362  aaliou3lem7  26400  dvradcnv  26471  pserdvlem2  26478  abssinper  26573  advlogexp  26707  atantayl3  26991  leibpilem2  26993  emcllem2  27048  harmonicbnd4  27062  basellem8  27139  ppiprm  27202  ppinprm  27203  chtprm  27204  chtnprm  27205  chpp1  27206  chtub  27263  perfectlem1  27280  perfectlem2  27281  perfect  27282  bcp1ctr  27330  lgsvalmod  27367  lgseisen  27430  lgsquadlem1  27431  lgsquad2lem1  27435  2sqlem10  27479  rplogsumlem1  27535  selberg2lem  27601  logdivbnd  27607  pntrsumo1  27616  pntpbnd2  27638  clwwlkf1  30207  subfacp1lem5  35494  subfacp1lem6  35495  subfacval2  35497  subfaclim  35498  cvmliftlem7  35601  cvmliftlem10  35604  mblfinlem2  38117  itg2addnclem3  38132  fdc  38204  mettrifi  38216  heiborlem4  38273  heiborlem6  38275  lzenom  43311  2nn0ind  43482  jm2.17a  43497  jm2.17b  43498  jm2.17c  43499  evensumeven  48289  perfectALTVlem2  48304  perfectALTV  48305