Theorem pncan 11451

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 489	. . 3 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → 𝐵 ∈ ℂ)
2		simpl 487	. . 3 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → 𝐴 ∈ ℂ)
3	1, 2	addcomd 11400	. 2 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐵 + 𝐴) = (𝐴 + 𝐵))
4		addcl 11170	. . 3 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 + 𝐵) ∈ ℂ)
5		subadd 11448	. . 3 ⊢ (((𝐴 + 𝐵) ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐴 ∈ ℂ) → (((𝐴 + 𝐵) − 𝐵) = 𝐴 ↔ (𝐵 + 𝐴) = (𝐴 + 𝐵)))
6	4, 1, 2, 5	syl3anc 1394	. 2 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (((𝐴 + 𝐵) − 𝐵) = 𝐴 ↔ (𝐵 + 𝐴) = (𝐴 + 𝐵)))
7	3, 6	mpbird 260	1 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((𝐴 + 𝐵) − 𝐵) = 𝐴)

Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 400   = wceq 1563   ∈ wcel 2145  (class class class)co 7400  ℂcc 11086   + caddc 11091   − cmin 11429

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1818  ax-4 1832  ax-5 1933  ax-6 1990  ax-7 2031  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2215  ax-ext 2737  ax-sep 5250  ax-nul 5260  ax-pow 5326  ax-pr 5394  ax-un 7722  ax-resscn 11145  ax-1cn 11146  ax-icn 11147  ax-addcl 11148  ax-addrcl 11149  ax-mulcl 11150  ax-mulrcl 11151  ax-mulcom 11152  ax-addass 11153  ax-mulass 11154  ax-distr 11155  ax-i2m1 11156  ax-1ne0 11157  ax-1rid 11158  ax-rnegex 11159  ax-rrecex 11160  ax-cnre 11161  ax-pre-lttri 11162  ax-pre-lttrn 11163  ax-pre-ltadd 11164

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3or 1102  df-3an 1103  df-tru 1566  df-fal 1576  df-ex 1803  df-nf 1807  df-sb 2094  df-mo 2569  df-eu 2599  df-clab 2744  df-cleq 2757  df-clel 2840  df-nfc 2914  df-ne 2961  df-nel 3065  df-ral 3080  df-rex 3090  df-reu 3371  df-rab 3418  df-v 3459  df-sbc 3748  df-csb 3856  df-dif 3910  df-un 3912  df-in 3914  df-ss 3924  df-nul 4289  df-if 4484  df-pw 4560  df-sn 4586  df-pr 4588  df-op 4592  df-uni 4868  df-br 5105  df-opab 5167  df-mpt 5186  df-id 5546  df-po 5559  df-so 5560  df-xp 5657  df-rel 5658  df-cnv 5659  df-co 5660  df-dm 5661  df-rn 5662  df-res 5663  df-ima 5664  df-iota 6481  df-fun 6527  df-fn 6528  df-f 6529  df-f1 6530  df-fo 6531  df-f1o 6532  df-fv 6533  df-riota 7357  df-ov 7403  df-oprab 7404  df-mpo 7405  df-er 8682  df-en 8932  df-dom 8933  df-sdom 8934  df-pnf 11233  df-mnf 11234  df-ltxr 11236  df-sub 11431

This theorem is referenced by:  pncan2  11452  addsubass  11455  pncan3oi  11461  subid1  11466  nppcan2  11477  pncand  11558  nn1m1nn  12242  nnsub  12268  elnn0nn  12534  elz2  12597  zrevaddcl  12627  nzadd  12630  qrevaddcl  12983  irradd  12985  fzrev3  13606  elfzp1b  13617  fzrevral3  13630  fzval3  13751  seqf1olem1  14065  seqf1olem2  14066  bcp1nk  14341  bcp1m1  14344  bcpasc  14345  hashbclem  14477  ccatalpha  14619  wrdind  14747  wrd2ind  14748  2cshwcshw  14850  shftlem  15093  shftval5  15103  isershft  15703  isercoll2  15708  mptfzshft  15817  telfsumo  15842  fsumparts  15846  bcxmas  15877  isum1p  15883  geolim  15912  mertenslem2  15927  mertens  15928  fsumkthpow  16098  eftlub  16153  effsumlt  16155  eirrlem  16248  dvdsadd  16348  prmind2  16731  iserodd  16883  fldivp1  16945  prmpwdvds  16952  pockthlem  16953  prmreclem4  16967  prmreclem6  16969  4sqlem11  17003  vdwapun  17022  ramub1lem1  17074  ramcl  17077  efgsval2  19791  efgsrel  19792  shft2rab  25624  uniioombllem3  25701  uniioombllem4  25702  dvexp  26069  dvfsumlem1  26142  degltp1le  26187  ply1divex  26251  plyaddlem1  26327  plymullem1  26328  dvply1  26402  dvply2g  26403  vieta1lem2  26429  aaliou3lem7  26467  dvradcnv  26538  pserdvlem2  26545  abssinper  26640  advlogexp  26774  atantayl3  27058  leibpilem2  27060  emcllem2  27115  harmonicbnd4  27129  basellem8  27206  ppiprm  27269  ppinprm  27270  chtprm  27271  chtnprm  27272  chpp1  27273  chtub  27330  perfectlem1  27347  perfectlem2  27348  perfect  27349  bcp1ctr  27397  lgsvalmod  27434  lgseisen  27497  lgsquadlem1  27498  lgsquad2lem1  27502  2sqlem10  27546  rplogsumlem1  27602  selberg2lem  27668  logdivbnd  27674  pntrsumo1  27683  pntpbnd2  27705  clwwlkf1  30305  subfacp1lem5  35542  subfacp1lem6  35543  subfacval2  35545  subfaclim  35546  cvmliftlem7  35649  cvmliftlem10  35652  mblfinlem2  38164  itg2addnclem3  38179  fdc  38251  mettrifi  38263  heiborlem4  38320  heiborlem6  38322  lzenom  43358  2nn0ind  43529  jm2.17a  43544  jm2.17b  43545  jm2.17c  43546  evensumeven  48328  perfectALTVlem2  48343  perfectALTV  48344