Theorem pncan 11387

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 484	. . 3 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → 𝐵 ∈ ℂ)
2		simpl 482	. . 3 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → 𝐴 ∈ ℂ)
3	1, 2	addcomd 11336	. 2 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐵 + 𝐴) = (𝐴 + 𝐵))
4		addcl 11110	. . 3 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 + 𝐵) ∈ ℂ)
5		subadd 11384	. . 3 ⊢ (((𝐴 + 𝐵) ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐴 ∈ ℂ) → (((𝐴 + 𝐵) − 𝐵) = 𝐴 ↔ (𝐵 + 𝐴) = (𝐴 + 𝐵)))
6	4, 1, 2, 5	syl3anc 1373	. 2 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (((𝐴 + 𝐵) − 𝐵) = 𝐴 ↔ (𝐵 + 𝐴) = (𝐴 + 𝐵)))
7	3, 6	mpbird 257	1 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((𝐴 + 𝐵) − 𝐵) = 𝐴)

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   = wceq 1540   ∈ wcel 2109  (class class class)co 7353  ℂcc 11026   + caddc 11031   − cmin 11365

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2701  ax-sep 5238  ax-nul 5248  ax-pow 5307  ax-pr 5374  ax-un 7675  ax-resscn 11085  ax-1cn 11086  ax-icn 11087  ax-addcl 11088  ax-addrcl 11089  ax-mulcl 11090  ax-mulrcl 11091  ax-mulcom 11092  ax-addass 11093  ax-mulass 11094  ax-distr 11095  ax-i2m1 11096  ax-1ne0 11097  ax-1rid 11098  ax-rnegex 11099  ax-rrecex 11100  ax-cnre 11101  ax-pre-lttri 11102  ax-pre-lttrn 11103  ax-pre-ltadd 11104

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2533  df-eu 2562  df-clab 2708  df-cleq 2721  df-clel 2803  df-nfc 2878  df-ne 2926  df-nel 3030  df-ral 3045  df-rex 3054  df-reu 3346  df-rab 3397  df-v 3440  df-sbc 3745  df-csb 3854  df-dif 3908  df-un 3910  df-in 3912  df-ss 3922  df-nul 4287  df-if 4479  df-pw 4555  df-sn 4580  df-pr 4582  df-op 4586  df-uni 4862  df-br 5096  df-opab 5158  df-mpt 5177  df-id 5518  df-po 5531  df-so 5532  df-xp 5629  df-rel 5630  df-cnv 5631  df-co 5632  df-dm 5633  df-rn 5634  df-res 5635  df-ima 5636  df-iota 6442  df-fun 6488  df-fn 6489  df-f 6490  df-f1 6491  df-fo 6492  df-f1o 6493  df-fv 6494  df-riota 7310  df-ov 7356  df-oprab 7357  df-mpo 7358  df-er 8632  df-en 8880  df-dom 8881  df-sdom 8882  df-pnf 11170  df-mnf 11171  df-ltxr 11173  df-sub 11367

This theorem is referenced by:  pncan2  11388  addsubass  11391  pncan3oi  11397  subid1  11402  nppcan2  11413  pncand  11494  nn1m1nn  12167  nnsub  12190  elnn0nn  12444  elz2  12507  zrevaddcl  12538  nzadd  12541  qrevaddcl  12890  irradd  12892  fzrev3  13511  elfzp1b  13522  fzrevral3  13535  fzval3  13655  seqf1olem1  13966  seqf1olem2  13967  bcp1nk  14242  bcp1m1  14245  bcpasc  14246  hashbclem  14377  ccatalpha  14518  wrdind  14646  wrd2ind  14647  2cshwcshw  14750  shftlem  14993  shftval5  15003  isershft  15589  isercoll2  15594  mptfzshft  15703  telfsumo  15727  fsumparts  15731  bcxmas  15760  isum1p  15766  geolim  15795  mertenslem2  15810  mertens  15811  fsumkthpow  15981  eftlub  16036  effsumlt  16038  eirrlem  16131  dvdsadd  16231  prmind2  16614  iserodd  16765  fldivp1  16827  prmpwdvds  16834  pockthlem  16835  prmreclem4  16849  prmreclem6  16851  4sqlem11  16885  vdwapun  16904  ramub1lem1  16956  ramcl  16959  efgsval2  19630  efgsrel  19631  shft2rab  25425  uniioombllem3  25502  uniioombllem4  25503  dvexp  25873  dvfsumlem1  25948  degltp1le  25994  ply1divex  26058  plyaddlem1  26134  plymullem1  26135  dvply1  26207  dvply2g  26208  dvply2gOLD  26209  vieta1lem2  26235  aaliou3lem7  26273  dvradcnv  26346  pserdvlem2  26354  abssinper  26446  advlogexp  26580  atantayl3  26865  leibpilem2  26867  emcllem2  26923  harmonicbnd4  26937  basellem8  27014  ppiprm  27077  ppinprm  27078  chtprm  27079  chtnprm  27080  chpp1  27081  chtub  27139  perfectlem1  27156  perfectlem2  27157  perfect  27158  bcp1ctr  27206  lgsvalmod  27243  lgseisen  27306  lgsquadlem1  27307  lgsquad2lem1  27311  2sqlem10  27355  rplogsumlem1  27411  selberg2lem  27477  logdivbnd  27483  pntrsumo1  27492  pntpbnd2  27514  clwwlkf1  30011  subfacp1lem5  35159  subfacp1lem6  35160  subfacval2  35162  subfaclim  35163  cvmliftlem7  35266  cvmliftlem10  35269  mblfinlem2  37640  itg2addnclem3  37655  fdc  37727  mettrifi  37739  heiborlem4  37796  heiborlem6  37798  lzenom  42746  2nn0ind  42921  jm2.17a  42936  jm2.17b  42937  jm2.17c  42938  evensumeven  47695  perfectALTVlem2  47710  perfectALTV  47711