Theorem pncan 11544

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 11493	. 2 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐵 + 𝐴) = (𝐴 + 𝐵))
4		addcl 11263	. . 3 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 + 𝐵) ∈ ℂ)
5		subadd 11541	. . 3 ⊢ (((𝐴 + 𝐵) ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐴 ∈ ℂ) → (((𝐴 + 𝐵) − 𝐵) = 𝐴 ↔ (𝐵 + 𝐴) = (𝐴 + 𝐵)))
6	4, 1, 2, 5	syl3anc 1398	. 2 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (((𝐴 + 𝐵) − 𝐵) = 𝐴 ↔ (𝐵 + 𝐴) = (𝐴 + 𝐵)))
7	3, 6	mpbird 260	1 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((𝐴 + 𝐵) − 𝐵) = 𝐴)

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∧ wa 401   = wceq 1570   ∈ wcel 2145  (class class class)co 7412  ℂcc 11179   + caddc 11184   − cmin 11522

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 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2213  ax-ext 2733  ax-sep 5249  ax-nul 5260  ax-pow 5327  ax-pr 5391  ax-un 7740  ax-resscn 11238  ax-1cn 11239  ax-icn 11240  ax-addcl 11241  ax-addrcl 11242  ax-mulcl 11243  ax-mulrcl 11244  ax-mulcom 11245  ax-addass 11246  ax-mulass 11247  ax-distr 11248  ax-i2m1 11249  ax-1ne0 11250  ax-1rid 11251  ax-rnegex 11252  ax-rrecex 11253  ax-cnre 11254  ax-pre-lttri 11255  ax-pre-lttrn 11256  ax-pre-ltadd 11257

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 2100  df-mo 2565  df-eu 2595  df-clab 2740  df-cleq 2753  df-clel 2836  df-nfc 2910  df-ne 2957  df-nel 3063  df-ral 3078  df-rex 3088  df-reu 3367  df-rab 3414  df-v 3453  df-sbc 3740  df-csb 3848  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-nul 4280  df-if 4483  df-pw 4559  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4868  df-br 5104  df-opab 5168  df-mpt 5187  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 6487  df-fun 6533  df-fn 6534  df-f 6535  df-f1 6536  df-fo 6537  df-f1o 6538  df-fv 6539  df-riota 7369  df-ov 7415  df-oprab 7416  df-mpo 7417  df-er 8701  df-en 8958  df-dom 8959  df-sdom 8960  df-pnf 11326  df-mnf 11327  df-ltxr 11329  df-sub 11524

This theorem is used by:  pncan2  11545  addsubass  11548  pncan3oi  11554  subid1  11559  nppcan2  11570  pncand  11651  nn1m1nn  12337  nnsub  12363  elnn0nn  12629  elz2  12692  zrevaddcl  12722  nzadd  12725  qrevaddcl  13080  irradd  13082  fzrev3  13704  elfzp1b  13715  fzrevral3  13728  fzval3  13849  seqf1olem1  14164  seqf1olem2  14165  bcp1nk  14441  bcp1m1  14444  bcpasc  14445  hashbclem  14577  ccatalpha  14720  wrdind  14851  wrd2ind  14852  2cshwcshw  14956  shftlem  15201  shftval5  15211  isershft  15811  isercoll2  15816  mptfzshft  15924  telfsumo  15949  fsumparts  15953  bcxmas  15984  isum1p  15990  geolim  16019  mertenslem2  16034  mertens  16035  fsumkthpow  16202  eftlub  16257  effsumlt  16259  eirrlem  16352  dvdsadd  16452  prmind2  16840  iserodd  16993  fldivp1  17055  prmpwdvds  17062  pockthlem  17063  prmreclem4  17077  prmreclem6  17079  4sqlem11  17113  vdwapun  17132  ramub1lem1  17184  ramcl  17187  efgsval2  19927  efgsrel  19928  shft2rab  25809  uniioombllem3  25886  uniioombllem4  25887  dvexp  26253  dvfsumlem1  26326  degltp1le  26371  ply1divex  26435  plyaddlem1  26512  plymullem1  26513  dvply1  26587  dvply2g  26588  vieta1lem2  26616  aaliou3lem7  26658  dvradcnv  26730  pserdvlem2  26737  abssinper  26831  advlogexp  26965  atantayl3  27249  leibpilem2  27251  emcllem2  27306  harmonicbnd4  27320  basellem8  27397  ppiprm  27460  ppinprm  27461  chtprm  27462  chtnprm  27463  chpp1  27464  chtub  27521  perfectlem1  27538  perfectlem2  27539  perfect  27540  bcp1ctr  27588  lgsvalmod  27625  lgseisen  27688  lgsquadlem1  27689  lgsquad2lem1  27693  2sqlem10  27737  rplogsumlem1  27793  selberg2lem  27859  logdivbnd  27865  pntrsumo1  27874  pntpbnd2  27896  clwwlkf1  30622  subfacp1lem5  35918  subfacp1lem6  35919  subfacval2  35921  subfaclim  35922  cvmliftlem7  36025  cvmliftlem10  36028  mblfinlem2  38544  itg2addnclem3  38559  fdc  38647  mettrifi  38659  heiborlem4  38716  heiborlem6  38718  lzenom  43734  2nn0ind  43905  jm2.17a  43920  jm2.17b  43921  jm2.17c  43922  evensumeven  48749  perfectALTVlem2  48764  perfectALTV  48765