Theorem pncan 11427

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

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   = wceq 1540   ∈ wcel 2109  (class class class)co 7387  ℂcc 11066   + caddc 11071   − cmin 11405

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2701  ax-sep 5251  ax-nul 5261  ax-pow 5320  ax-pr 5387  ax-un 7711  ax-resscn 11125  ax-1cn 11126  ax-icn 11127  ax-addcl 11128  ax-addrcl 11129  ax-mulcl 11130  ax-mulrcl 11131  ax-mulcom 11132  ax-addass 11133  ax-mulass 11134  ax-distr 11135  ax-i2m1 11136  ax-1ne0 11137  ax-1rid 11138  ax-rnegex 11139  ax-rrecex 11140  ax-cnre 11141  ax-pre-lttri 11142  ax-pre-lttrn 11143  ax-pre-ltadd 11144

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2533  df-eu 2562  df-clab 2708  df-cleq 2721  df-clel 2803  df-nfc 2878  df-ne 2926  df-nel 3030  df-ral 3045  df-rex 3054  df-reu 3355  df-rab 3406  df-v 3449  df-sbc 3754  df-csb 3863  df-dif 3917  df-un 3919  df-in 3921  df-ss 3931  df-nul 4297  df-if 4489  df-pw 4565  df-sn 4590  df-pr 4592  df-op 4596  df-uni 4872  df-br 5108  df-opab 5170  df-mpt 5189  df-id 5533  df-po 5546  df-so 5547  df-xp 5644  df-rel 5645  df-cnv 5646  df-co 5647  df-dm 5648  df-rn 5649  df-res 5650  df-ima 5651  df-iota 6464  df-fun 6513  df-fn 6514  df-f 6515  df-f1 6516  df-fo 6517  df-f1o 6518  df-fv 6519  df-riota 7344  df-ov 7390  df-oprab 7391  df-mpo 7392  df-er 8671  df-en 8919  df-dom 8920  df-sdom 8921  df-pnf 11210  df-mnf 11211  df-ltxr 11213  df-sub 11407

This theorem is referenced by:  pncan2  11428  addsubass  11431  pncan3oi  11437  subid1  11442  nppcan2  11453  pncand  11534  nn1m1nn  12207  nnsub  12230  elnn0nn  12484  elz2  12547  zrevaddcl  12578  nzadd  12581  qrevaddcl  12930  irradd  12932  fzrev3  13551  elfzp1b  13562  fzrevral3  13575  fzval3  13695  seqf1olem1  14006  seqf1olem2  14007  bcp1nk  14282  bcp1m1  14285  bcpasc  14286  hashbclem  14417  ccatalpha  14558  wrdind  14687  wrd2ind  14688  2cshwcshw  14791  shftlem  15034  shftval5  15044  isershft  15630  isercoll2  15635  mptfzshft  15744  telfsumo  15768  fsumparts  15772  bcxmas  15801  isum1p  15807  geolim  15836  mertenslem2  15851  mertens  15852  fsumkthpow  16022  eftlub  16077  effsumlt  16079  eirrlem  16172  dvdsadd  16272  prmind2  16655  iserodd  16806  fldivp1  16868  prmpwdvds  16875  pockthlem  16876  prmreclem4  16890  prmreclem6  16892  4sqlem11  16926  vdwapun  16945  ramub1lem1  16997  ramcl  17000  efgsval2  19663  efgsrel  19664  shft2rab  25409  uniioombllem3  25486  uniioombllem4  25487  dvexp  25857  dvfsumlem1  25932  degltp1le  25978  ply1divex  26042  plyaddlem1  26118  plymullem1  26119  dvply1  26191  dvply2g  26192  dvply2gOLD  26193  vieta1lem2  26219  aaliou3lem7  26257  dvradcnv  26330  pserdvlem2  26338  abssinper  26430  advlogexp  26564  atantayl3  26849  leibpilem2  26851  emcllem2  26907  harmonicbnd4  26921  basellem8  26998  ppiprm  27061  ppinprm  27062  chtprm  27063  chtnprm  27064  chpp1  27065  chtub  27123  perfectlem1  27140  perfectlem2  27141  perfect  27142  bcp1ctr  27190  lgsvalmod  27227  lgseisen  27290  lgsquadlem1  27291  lgsquad2lem1  27295  2sqlem10  27339  rplogsumlem1  27395  selberg2lem  27461  logdivbnd  27467  pntrsumo1  27476  pntpbnd2  27498  clwwlkf1  29978  subfacp1lem5  35171  subfacp1lem6  35172  subfacval2  35174  subfaclim  35175  cvmliftlem7  35278  cvmliftlem10  35281  mblfinlem2  37652  itg2addnclem3  37667  fdc  37739  mettrifi  37751  heiborlem4  37808  heiborlem6  37810  lzenom  42758  2nn0ind  42934  jm2.17a  42949  jm2.17b  42950  jm2.17c  42951  evensumeven  47708  perfectALTVlem2  47723  perfectALTV  47724