Theorem pncan 11593

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 490	. . 3 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → 𝐵 ∈ ℂ)
2		simpl 488	. . 3 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → 𝐴 ∈ ℂ)
3	1, 2	addcomd 11542	. 2 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐵 + 𝐴) = (𝐴 + 𝐵))
4		addcl 11312	. . 3 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 + 𝐵) ∈ ℂ)
5		subadd 11590	. . 3 ⊢ (((𝐴 + 𝐵) ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐴 ∈ ℂ) → (((𝐴 + 𝐵) − 𝐵) = 𝐴 ↔ (𝐵 + 𝐴) = (𝐴 + 𝐵)))
6	4, 1, 2, 5	syl3anc 1399	. 2 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (((𝐴 + 𝐵) − 𝐵) = 𝐴 ↔ (𝐵 + 𝐴) = (𝐴 + 𝐵)))
7	3, 6	mpbird 260	1 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((𝐴 + 𝐵) − 𝐵) = 𝐴)

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∧ wa 401   = wceq 1570   ∈ wcel 2147  (class class class)co 7446  ℂcc 11228   + caddc 11233   − cmin 11571

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-10 2180  ax-11 2197  ax-12 2216  ax-ext 2735  ax-sep 5253  ax-nul 5264  ax-pow 5332  ax-pr 5396  ax-un 7778  ax-resscn 11287  ax-1cn 11288  ax-icn 11289  ax-addcl 11290  ax-addrcl 11291  ax-mulcl 11292  ax-mulrcl 11293  ax-mulcom 11294  ax-addass 11295  ax-mulass 11296  ax-distr 11297  ax-i2m1 11298  ax-1ne0 11299  ax-1rid 11300  ax-rnegex 11301  ax-rrecex 11302  ax-cnre 11303  ax-pre-lttri 11304  ax-pre-lttrn 11305  ax-pre-ltadd 11306

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2102  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2839  df-nfc 2913  df-ne 2960  df-nel 3066  df-ral 3081  df-rex 3091  df-reu 3370  df-rab 3417  df-v 3456  df-sbc 3743  df-csb 3852  df-ss 3901  df-dif 4050  df-in 4094  df-un 4154  df-nul 4282  df-if 4486  df-pw 4562  df-sn 4589  df-pr 4591  df-op 4839  df-uni 4871  df-br 5107  df-opab 5172  df-mpt 5191  df-id 5551  df-po 5564  df-so 5565  df-xp 5662  df-rel 5663  df-cnv 5664  df-co 5665  df-dm 5666  df-rn 5667  df-res 5668  df-ima 5669  df-iota 6515  df-fun 6563  df-fn 6564  df-f 6565  df-f1 6566  df-fo 6567  df-f1o 6568  df-fv 6569  df-riota 7403  df-ov 7449  df-oprab 7450  df-mpo 7451  df-er 8748  df-en 9005  df-dom 9006  df-sdom 9007  df-pnf 11375  df-mnf 11376  df-ltxr 11378  df-sub 11573

This theorem is used by:  pncan2  11594  addsubass  11597  pncan3oi  11603  subid1  11608  nppcan2  11619  pncand  11700  nn1m1nn  12386  nnsub  12412  elnn0nn  12678  elz2  12741  zrevaddcl  12771  nzadd  12774  qrevaddcl  13129  irradd  13131  fzrev3  13754  elfzp1b  13765  fzrevral3  13778  fzval3  13899  seqf1olem1  14214  seqf1olem2  14215  bcp1nk  14491  bcp1m1  14494  bcpasc  14495  hashbclem  14627  ccatalpha  14770  wrdind  14902  wrd2ind  14903  2cshwcshw  15007  shftlem  15253  shftval5  15263  isershft  15863  isercoll2  15868  mptfzshft  15976  telfsumo  16001  fsumparts  16005  bcxmas  16036  isum1p  16042  geolim  16071  mertenslem2  16086  mertens  16087  fsumkthpow  16254  eftlub  16309  effsumlt  16311  eirrlem  16404  dvdsadd  16504  prmind2  16892  iserodd  17045  fldivp1  17107  prmpwdvds  17114  pockthlem  17115  prmreclem4  17129  prmreclem6  17131  4sqlem11  17165  vdwapun  17184  ramub1lem1  17236  ramcl  17239  efgsval2  19980  efgsrel  19981  shft2rab  25862  uniioombllem3  25939  uniioombllem4  25940  dvexp  26306  dvfsumlem1  26379  degltp1le  26424  ply1divex  26488  plyaddlem1  26565  plymullem1  26566  dvply1  26638  dvply2g  26639  vieta1lem2  26667  aaliou3lem7  26709  dvradcnv  26781  pserdvlem2  26788  abssinper  26882  advlogexp  27016  atantayl3  27300  leibpilem2  27302  emcllem2  27357  harmonicbnd4  27371  basellem8  27448  ppiprm  27511  ppinprm  27512  chtprm  27513  chtnprm  27514  chpp1  27515  chtub  27572  perfectlem1  27589  perfectlem2  27590  perfect  27591  bcp1ctr  27639  lgsvalmod  27676  lgseisen  27739  lgsquadlem1  27740  lgsquad2lem1  27744  2sqlem10  27788  rplogsumlem1  27844  selberg2lem  27910  logdivbnd  27916  pntrsumo1  27925  pntpbnd2  27947  clwwlkf1  30673  subfacp1lem5  36129  subfacp1lem6  36130  subfacval2  36132  subfaclim  36133  cvmliftlem7  36236  cvmliftlem10  36239  mblfinlem2  38781  itg2addnclem3  38796  fdc  38882  mettrifi  38894  heiborlem4  38951  heiborlem6  38953  lzenom  43985  2nn0ind  44156  jm2.17a  44171  jm2.17b  44172  jm2.17c  44173  evensumeven  49020  perfectALTVlem2  49035  perfectALTV  49036