Theorem pncan 11398

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

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   = wceq 1542   ∈ wcel 2114  (class class class)co 7368  ℂcc 11036   + caddc 11041   − cmin 11376

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2709  ax-sep 5243  ax-nul 5253  ax-pow 5312  ax-pr 5379  ax-un 7690  ax-resscn 11095  ax-1cn 11096  ax-icn 11097  ax-addcl 11098  ax-addrcl 11099  ax-mulcl 11100  ax-mulrcl 11101  ax-mulcom 11102  ax-addass 11103  ax-mulass 11104  ax-distr 11105  ax-i2m1 11106  ax-1ne0 11107  ax-1rid 11108  ax-rnegex 11109  ax-rrecex 11110  ax-cnre 11111  ax-pre-lttri 11112  ax-pre-lttrn 11113  ax-pre-ltadd 11114

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2540  df-eu 2570  df-clab 2716  df-cleq 2729  df-clel 2812  df-nfc 2886  df-ne 2934  df-nel 3038  df-ral 3053  df-rex 3063  df-reu 3353  df-rab 3402  df-v 3444  df-sbc 3743  df-csb 3852  df-dif 3906  df-un 3908  df-in 3910  df-ss 3920  df-nul 4288  df-if 4482  df-pw 4558  df-sn 4583  df-pr 4585  df-op 4589  df-uni 4866  df-br 5101  df-opab 5163  df-mpt 5182  df-id 5527  df-po 5540  df-so 5541  df-xp 5638  df-rel 5639  df-cnv 5640  df-co 5641  df-dm 5642  df-rn 5643  df-res 5644  df-ima 5645  df-iota 6456  df-fun 6502  df-fn 6503  df-f 6504  df-f1 6505  df-fo 6506  df-f1o 6507  df-fv 6508  df-riota 7325  df-ov 7371  df-oprab 7372  df-mpo 7373  df-er 8645  df-en 8896  df-dom 8897  df-sdom 8898  df-pnf 11180  df-mnf 11181  df-ltxr 11183  df-sub 11378

This theorem is referenced by:  pncan2  11399  addsubass  11402  pncan3oi  11408  subid1  11413  nppcan2  11424  pncand  11505  nn1m1nn  12178  nnsub  12201  elnn0nn  12455  elz2  12518  zrevaddcl  12548  nzadd  12551  qrevaddcl  12896  irradd  12898  fzrev3  13518  elfzp1b  13529  fzrevral3  13542  fzval3  13662  seqf1olem1  13976  seqf1olem2  13977  bcp1nk  14252  bcp1m1  14255  bcpasc  14256  hashbclem  14387  ccatalpha  14529  wrdind  14657  wrd2ind  14658  2cshwcshw  14760  shftlem  15003  shftval5  15013  isershft  15599  isercoll2  15604  mptfzshft  15713  telfsumo  15737  fsumparts  15741  bcxmas  15770  isum1p  15776  geolim  15805  mertenslem2  15820  mertens  15821  fsumkthpow  15991  eftlub  16046  effsumlt  16048  eirrlem  16141  dvdsadd  16241  prmind2  16624  iserodd  16775  fldivp1  16837  prmpwdvds  16844  pockthlem  16845  prmreclem4  16859  prmreclem6  16861  4sqlem11  16895  vdwapun  16914  ramub1lem1  16966  ramcl  16969  efgsval2  19674  efgsrel  19675  shft2rab  25477  uniioombllem3  25554  uniioombllem4  25555  dvexp  25925  dvfsumlem1  26000  degltp1le  26046  ply1divex  26110  plyaddlem1  26186  plymullem1  26187  dvply1  26259  dvply2g  26260  dvply2gOLD  26261  vieta1lem2  26287  aaliou3lem7  26325  dvradcnv  26398  pserdvlem2  26406  abssinper  26498  advlogexp  26632  atantayl3  26917  leibpilem2  26919  emcllem2  26975  harmonicbnd4  26989  basellem8  27066  ppiprm  27129  ppinprm  27130  chtprm  27131  chtnprm  27132  chpp1  27133  chtub  27191  perfectlem1  27208  perfectlem2  27209  perfect  27210  bcp1ctr  27258  lgsvalmod  27295  lgseisen  27358  lgsquadlem1  27359  lgsquad2lem1  27363  2sqlem10  27407  rplogsumlem1  27463  selberg2lem  27529  logdivbnd  27535  pntrsumo1  27544  pntpbnd2  27566  clwwlkf1  30136  subfacp1lem5  35397  subfacp1lem6  35398  subfacval2  35400  subfaclim  35401  cvmliftlem7  35504  cvmliftlem10  35507  mblfinlem2  37906  itg2addnclem3  37921  fdc  37993  mettrifi  38005  heiborlem4  38062  heiborlem6  38064  lzenom  43124  2nn0ind  43299  jm2.17a  43314  jm2.17b  43315  jm2.17c  43316  evensumeven  48064  perfectALTVlem2  48079  perfectALTV  48080