Theorem pncan 11511

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 11460	. 2 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐵 + 𝐴) = (𝐴 + 𝐵))
4		addcl 11234	. . 3 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 + 𝐵) ∈ ℂ)
5		subadd 11508	. . 3 ⊢ (((𝐴 + 𝐵) ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐴 ∈ ℂ) → (((𝐴 + 𝐵) − 𝐵) = 𝐴 ↔ (𝐵 + 𝐴) = (𝐴 + 𝐵)))
6	4, 1, 2, 5	syl3anc 1370	. 2 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (((𝐴 + 𝐵) − 𝐵) = 𝐴 ↔ (𝐵 + 𝐴) = (𝐴 + 𝐵)))
7	3, 6	mpbird 257	1 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((𝐴 + 𝐵) − 𝐵) = 𝐴)

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   = wceq 1536   ∈ wcel 2105  (class class class)co 7430  ℂcc 11150   + caddc 11155   − cmin 11489

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-10 2138  ax-11 2154  ax-12 2174  ax-ext 2705  ax-sep 5301  ax-nul 5311  ax-pow 5370  ax-pr 5437  ax-un 7753  ax-resscn 11209  ax-1cn 11210  ax-icn 11211  ax-addcl 11212  ax-addrcl 11213  ax-mulcl 11214  ax-mulrcl 11215  ax-mulcom 11216  ax-addass 11217  ax-mulass 11218  ax-distr 11219  ax-i2m1 11220  ax-1ne0 11221  ax-1rid 11222  ax-rnegex 11223  ax-rrecex 11224  ax-cnre 11225  ax-pre-lttri 11226  ax-pre-lttrn 11227  ax-pre-ltadd 11228

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1539  df-fal 1549  df-ex 1776  df-nf 1780  df-sb 2062  df-mo 2537  df-eu 2566  df-clab 2712  df-cleq 2726  df-clel 2813  df-nfc 2889  df-ne 2938  df-nel 3044  df-ral 3059  df-rex 3068  df-reu 3378  df-rab 3433  df-v 3479  df-sbc 3791  df-csb 3908  df-dif 3965  df-un 3967  df-in 3969  df-ss 3979  df-nul 4339  df-if 4531  df-pw 4606  df-sn 4631  df-pr 4633  df-op 4637  df-uni 4912  df-br 5148  df-opab 5210  df-mpt 5231  df-id 5582  df-po 5596  df-so 5597  df-xp 5694  df-rel 5695  df-cnv 5696  df-co 5697  df-dm 5698  df-rn 5699  df-res 5700  df-ima 5701  df-iota 6515  df-fun 6564  df-fn 6565  df-f 6566  df-f1 6567  df-fo 6568  df-f1o 6569  df-fv 6570  df-riota 7387  df-ov 7433  df-oprab 7434  df-mpo 7435  df-er 8743  df-en 8984  df-dom 8985  df-sdom 8986  df-pnf 11294  df-mnf 11295  df-ltxr 11297  df-sub 11491

This theorem is referenced by:  pncan2  11512  addsubass  11515  pncan3oi  11521  subid1  11526  nppcan2  11537  pncand  11618  nn1m1nn  12284  nnsub  12307  elnn0nn  12565  elz2  12628  zrevaddcl  12659  nzadd  12662  qrevaddcl  13010  irradd  13012  fzrev3  13626  elfzp1b  13637  fzrevral3  13650  fzval3  13769  seqf1olem1  14078  seqf1olem2  14079  bcp1nk  14352  bcp1m1  14355  bcpasc  14356  hashbclem  14487  ccatalpha  14627  wrdind  14756  wrd2ind  14757  2cshwcshw  14860  shftlem  15103  shftval5  15113  isershft  15696  isercoll2  15701  mptfzshft  15810  telfsumo  15834  fsumparts  15838  bcxmas  15867  isum1p  15873  geolim  15902  mertenslem2  15917  mertens  15918  fsumkthpow  16088  eftlub  16141  effsumlt  16143  eirrlem  16236  dvdsadd  16335  prmind2  16718  iserodd  16868  fldivp1  16930  prmpwdvds  16937  pockthlem  16938  prmreclem4  16952  prmreclem6  16954  4sqlem11  16988  vdwapun  17007  ramub1lem1  17059  ramcl  17062  efgsval2  19765  efgsrel  19766  shft2rab  25556  uniioombllem3  25633  uniioombllem4  25634  dvexp  26005  dvfsumlem1  26080  degltp1le  26126  ply1divex  26190  plyaddlem1  26266  plymullem1  26267  dvply1  26339  dvply2g  26340  dvply2gOLD  26341  vieta1lem2  26367  aaliou3lem7  26405  dvradcnv  26478  pserdvlem2  26486  abssinper  26577  advlogexp  26711  atantayl3  26996  leibpilem2  26998  emcllem2  27054  harmonicbnd4  27068  basellem8  27145  ppiprm  27208  ppinprm  27209  chtprm  27210  chtnprm  27211  chpp1  27212  chtub  27270  perfectlem1  27287  perfectlem2  27288  perfect  27289  bcp1ctr  27337  lgsvalmod  27374  lgseisen  27437  lgsquadlem1  27438  lgsquad2lem1  27442  2sqlem10  27486  rplogsumlem1  27542  selberg2lem  27608  logdivbnd  27614  pntrsumo1  27623  pntpbnd2  27645  clwwlkf1  30077  subfacp1lem5  35168  subfacp1lem6  35169  subfacval2  35171  subfaclim  35172  cvmliftlem7  35275  cvmliftlem10  35278  mblfinlem2  37644  itg2addnclem3  37659  fdc  37731  mettrifi  37743  heiborlem4  37800  heiborlem6  37802  lzenom  42757  2nn0ind  42933  jm2.17a  42948  jm2.17b  42949  jm2.17c  42950  evensumeven  47631  perfectALTVlem2  47646  perfectALTV  47647