Theorem pncan 11237

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 485	. . 3 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → 𝐵 ∈ ℂ)
2		simpl 483	. . 3 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → 𝐴 ∈ ℂ)
3	1, 2	addcomd 11187	. 2 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐵 + 𝐴) = (𝐴 + 𝐵))
4		addcl 10963	. . 3 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 + 𝐵) ∈ ℂ)
5		subadd 11234	. . 3 ⊢ (((𝐴 + 𝐵) ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐴 ∈ ℂ) → (((𝐴 + 𝐵) − 𝐵) = 𝐴 ↔ (𝐵 + 𝐴) = (𝐴 + 𝐵)))
6	4, 1, 2, 5	syl3anc 1370	. 2 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (((𝐴 + 𝐵) − 𝐵) = 𝐴 ↔ (𝐵 + 𝐴) = (𝐴 + 𝐵)))
7	3, 6	mpbird 256	1 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((𝐴 + 𝐵) − 𝐵) = 𝐴)

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 396   = wceq 1539   ∈ wcel 2106  (class class class)co 7267  ℂcc 10879   + caddc 10884   − cmin 11215

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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2709  ax-sep 5221  ax-nul 5228  ax-pow 5286  ax-pr 5350  ax-un 7578  ax-resscn 10938  ax-1cn 10939  ax-icn 10940  ax-addcl 10941  ax-addrcl 10942  ax-mulcl 10943  ax-mulrcl 10944  ax-mulcom 10945  ax-addass 10946  ax-mulass 10947  ax-distr 10948  ax-i2m1 10949  ax-1ne0 10950  ax-1rid 10951  ax-rnegex 10952  ax-rrecex 10953  ax-cnre 10954  ax-pre-lttri 10955  ax-pre-lttrn 10956  ax-pre-ltadd 10957

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3or 1087  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1783  df-nf 1787  df-sb 2068  df-mo 2540  df-eu 2569  df-clab 2716  df-cleq 2730  df-clel 2816  df-nfc 2889  df-ne 2944  df-nel 3050  df-ral 3069  df-rex 3070  df-reu 3071  df-rab 3073  df-v 3431  df-sbc 3716  df-csb 3832  df-dif 3889  df-un 3891  df-in 3893  df-ss 3903  df-nul 4257  df-if 4460  df-pw 4535  df-sn 4562  df-pr 4564  df-op 4568  df-uni 4840  df-br 5074  df-opab 5136  df-mpt 5157  df-id 5484  df-po 5498  df-so 5499  df-xp 5590  df-rel 5591  df-cnv 5592  df-co 5593  df-dm 5594  df-rn 5595  df-res 5596  df-ima 5597  df-iota 6384  df-fun 6428  df-fn 6429  df-f 6430  df-f1 6431  df-fo 6432  df-f1o 6433  df-fv 6434  df-riota 7224  df-ov 7270  df-oprab 7271  df-mpo 7272  df-er 8485  df-en 8721  df-dom 8722  df-sdom 8723  df-pnf 11021  df-mnf 11022  df-ltxr 11024  df-sub 11217

This theorem is referenced by:  pncan2  11238  addsubass  11241  pncan3oi  11247  subid1  11251  nppcan2  11262  pncand  11343  nn1m1nn  12004  nnsub  12027  elnn0nn  12285  elz2  12347  zrevaddcl  12375  nzadd  12378  qrevaddcl  12721  irradd  12723  fzrev3  13332  elfzp1b  13343  fzrevral3  13353  fzval3  13466  seqf1olem1  13772  seqf1olem2  13773  bcp1nk  14041  bcp1m1  14044  bcpasc  14045  hashbclem  14174  ccatalpha  14308  wrdind  14445  wrd2ind  14446  2cshwcshw  14548  shftlem  14789  shftval5  14799  isershft  15385  isercoll2  15390  fsump1  15478  mptfzshft  15500  telfsumo  15524  fsumparts  15528  bcxmas  15557  isum1p  15563  geolim  15592  mertenslem2  15607  mertens  15608  fsumkthpow  15776  eftlub  15828  effsumlt  15830  eirrlem  15923  dvdsadd  16021  prmind2  16400  iserodd  16546  fldivp1  16608  prmpwdvds  16615  pockthlem  16616  prmreclem4  16630  prmreclem6  16632  4sqlem11  16666  vdwapun  16685  ramub1lem1  16737  ramcl  16740  efgsval2  19349  efgsrel  19350  shft2rab  24682  uniioombllem3  24759  uniioombllem4  24760  dvexp  25127  dvfsumlem1  25200  degltp1le  25248  ply1divex  25311  plyaddlem1  25384  plymullem1  25385  dvply1  25454  dvply2g  25455  vieta1lem2  25481  aaliou3lem7  25519  dvradcnv  25590  pserdvlem2  25597  abssinper  25687  advlogexp  25820  atantayl3  26099  leibpilem2  26101  emcllem2  26156  harmonicbnd4  26170  basellem8  26247  ppiprm  26310  ppinprm  26311  chtprm  26312  chtnprm  26313  chpp1  26314  chtub  26370  perfectlem1  26387  perfectlem2  26388  perfect  26389  bcp1ctr  26437  lgsvalmod  26474  lgseisen  26537  lgsquadlem1  26538  lgsquad2lem1  26542  2sqlem10  26586  rplogsumlem1  26642  selberg2lem  26708  logdivbnd  26714  pntrsumo1  26723  pntpbnd2  26745  clwwlkf1  28421  subfacp1lem5  33154  subfacp1lem6  33155  subfacval2  33157  subfaclim  33158  cvmliftlem7  33261  cvmliftlem10  33264  mblfinlem2  35823  itg2addnclem3  35838  fdc  35911  mettrifi  35923  heiborlem4  35980  heiborlem6  35982  lzenom  40600  2nn0ind  40775  jm2.17a  40790  jm2.17b  40791  jm2.17c  40792  evensumeven  45137  perfectALTVlem2  45152  perfectALTV  45153