Theorem pncan 11157

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 11107	. 2 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐵 + 𝐴) = (𝐴 + 𝐵))
4		addcl 10884	. . 3 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 + 𝐵) ∈ ℂ)
5		subadd 11154	. . 3 ⊢ (((𝐴 + 𝐵) ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐴 ∈ ℂ) → (((𝐴 + 𝐵) − 𝐵) = 𝐴 ↔ (𝐵 + 𝐴) = (𝐴 + 𝐵)))
6	4, 1, 2, 5	syl3anc 1369	. 2 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (((𝐴 + 𝐵) − 𝐵) = 𝐴 ↔ (𝐵 + 𝐴) = (𝐴 + 𝐵)))
7	3, 6	mpbird 256	1 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((𝐴 + 𝐵) − 𝐵) = 𝐴)

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 395   = wceq 1539   ∈ wcel 2108  (class class class)co 7255  ℂcc 10800   + caddc 10805   − cmin 11135

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-10 2139  ax-11 2156  ax-12 2173  ax-ext 2709  ax-sep 5218  ax-nul 5225  ax-pow 5283  ax-pr 5347  ax-un 7566  ax-resscn 10859  ax-1cn 10860  ax-icn 10861  ax-addcl 10862  ax-addrcl 10863  ax-mulcl 10864  ax-mulrcl 10865  ax-mulcom 10866  ax-addass 10867  ax-mulass 10868  ax-distr 10869  ax-i2m1 10870  ax-1ne0 10871  ax-1rid 10872  ax-rnegex 10873  ax-rrecex 10874  ax-cnre 10875  ax-pre-lttri 10876  ax-pre-lttrn 10877  ax-pre-ltadd 10878

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-3or 1086  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1784  df-nf 1788  df-sb 2069  df-mo 2540  df-eu 2569  df-clab 2716  df-cleq 2730  df-clel 2817  df-nfc 2888  df-ne 2943  df-nel 3049  df-ral 3068  df-rex 3069  df-reu 3070  df-rab 3072  df-v 3424  df-sbc 3712  df-csb 3829  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-nul 4254  df-if 4457  df-pw 4532  df-sn 4559  df-pr 4561  df-op 4565  df-uni 4837  df-br 5071  df-opab 5133  df-mpt 5154  df-id 5480  df-po 5494  df-so 5495  df-xp 5586  df-rel 5587  df-cnv 5588  df-co 5589  df-dm 5590  df-rn 5591  df-res 5592  df-ima 5593  df-iota 6376  df-fun 6420  df-fn 6421  df-f 6422  df-f1 6423  df-fo 6424  df-f1o 6425  df-fv 6426  df-riota 7212  df-ov 7258  df-oprab 7259  df-mpo 7260  df-er 8456  df-en 8692  df-dom 8693  df-sdom 8694  df-pnf 10942  df-mnf 10943  df-ltxr 10945  df-sub 11137

This theorem is referenced by:  pncan2  11158  addsubass  11161  pncan3oi  11167  subid1  11171  nppcan2  11182  pncand  11263  nn1m1nn  11924  nnsub  11947  elnn0nn  12205  elz2  12267  zrevaddcl  12295  nzadd  12298  qrevaddcl  12640  irradd  12642  fzrev3  13251  elfzp1b  13262  fzrevral3  13272  fzval3  13384  seqf1olem1  13690  seqf1olem2  13691  bcp1nk  13959  bcp1m1  13962  bcpasc  13963  hashbclem  14092  ccatalpha  14226  wrdind  14363  wrd2ind  14364  2cshwcshw  14466  shftlem  14707  shftval5  14717  isershft  15303  isercoll2  15308  fsump1  15396  mptfzshft  15418  telfsumo  15442  fsumparts  15446  bcxmas  15475  isum1p  15481  geolim  15510  mertenslem2  15525  mertens  15526  fsumkthpow  15694  eftlub  15746  effsumlt  15748  eirrlem  15841  dvdsadd  15939  prmind2  16318  iserodd  16464  fldivp1  16526  prmpwdvds  16533  pockthlem  16534  prmreclem4  16548  prmreclem6  16550  4sqlem11  16584  vdwapun  16603  ramub1lem1  16655  ramcl  16658  efgsval2  19254  efgsrel  19255  shft2rab  24577  uniioombllem3  24654  uniioombllem4  24655  dvexp  25022  dvfsumlem1  25095  degltp1le  25143  ply1divex  25206  plyaddlem1  25279  plymullem1  25280  dvply1  25349  dvply2g  25350  vieta1lem2  25376  aaliou3lem7  25414  dvradcnv  25485  pserdvlem2  25492  abssinper  25582  advlogexp  25715  atantayl3  25994  leibpilem2  25996  emcllem2  26051  harmonicbnd4  26065  basellem8  26142  ppiprm  26205  ppinprm  26206  chtprm  26207  chtnprm  26208  chpp1  26209  chtub  26265  perfectlem1  26282  perfectlem2  26283  perfect  26284  bcp1ctr  26332  lgsvalmod  26369  lgseisen  26432  lgsquadlem1  26433  lgsquad2lem1  26437  2sqlem10  26481  rplogsumlem1  26537  selberg2lem  26603  logdivbnd  26609  pntrsumo1  26618  pntpbnd2  26640  clwwlkf1  28314  subfacp1lem5  33046  subfacp1lem6  33047  subfacval2  33049  subfaclim  33050  cvmliftlem7  33153  cvmliftlem10  33156  mblfinlem2  35742  itg2addnclem3  35757  fdc  35830  mettrifi  35842  heiborlem4  35899  heiborlem6  35901  lzenom  40508  2nn0ind  40683  jm2.17a  40698  jm2.17b  40699  jm2.17c  40700  evensumeven  45047  perfectALTVlem2  45062  perfectALTV  45063