Theorem npcan 7745

Description: Cancellation law for subtraction. (Contributed by NM, 10-May-2004.) (Revised by Mario Carneiro, 27-May-2016.)

Assertion

Ref	Expression
npcan	⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((𝐴 − 𝐵) + 𝐵) = 𝐴)

Proof of Theorem npcan

Step	Hyp	Ref	Expression
1		subcl 7735	. . 3 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 − 𝐵) ∈ ℂ)
2		simpr 109	. . 3 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → 𝐵 ∈ ℂ)
3	1, 2	addcomd 7687	. 2 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((𝐴 − 𝐵) + 𝐵) = (𝐵 + (𝐴 − 𝐵)))
4		pncan3 7744	. . 3 ⊢ ((𝐵 ∈ ℂ ∧ 𝐴 ∈ ℂ) → (𝐵 + (𝐴 − 𝐵)) = 𝐴)
5	4	ancoms 265	. 2 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐵 + (𝐴 − 𝐵)) = 𝐴)
6	3, 5	eqtrd 2121	1 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((𝐴 − 𝐵) + 𝐵) = 𝐴)

Syntax hints:   → wi 4   ∧ wa 103   = wceq 1290   ∈ wcel 1439  (class class class)co 5666  ℂcc 7402   + caddc 7407   − cmin 7707

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-in1 580  ax-in2 581  ax-io 666  ax-5 1382  ax-7 1383  ax-gen 1384  ax-ie1 1428  ax-ie2 1429  ax-8 1441  ax-10 1442  ax-11 1443  ax-i12 1444  ax-bndl 1445  ax-4 1446  ax-14 1451  ax-17 1465  ax-i9 1469  ax-ial 1473  ax-i5r 1474  ax-ext 2071  ax-sep 3963  ax-pow 4015  ax-pr 4045  ax-setind 4366  ax-resscn 7491  ax-1cn 7492  ax-icn 7494  ax-addcl 7495  ax-addrcl 7496  ax-mulcl 7497  ax-addcom 7499  ax-addass 7501  ax-distr 7503  ax-i2m1 7504  ax-0id 7507  ax-rnegex 7508  ax-cnre 7510

This theorem depends on definitions:  df-bi 116  df-3an 927  df-tru 1293  df-fal 1296  df-nf 1396  df-sb 1694  df-eu 1952  df-mo 1953  df-clab 2076  df-cleq 2082  df-clel 2085  df-nfc 2218  df-ne 2257  df-ral 2365  df-rex 2366  df-reu 2367  df-rab 2369  df-v 2622  df-sbc 2842  df-dif 3002  df-un 3004  df-in 3006  df-ss 3013  df-pw 3435  df-sn 3456  df-pr 3457  df-op 3459  df-uni 3660  df-br 3852  df-opab 3906  df-id 4129  df-xp 4457  df-rel 4458  df-cnv 4459  df-co 4460  df-dm 4461  df-iota 4993  df-fun 5030  df-fv 5036  df-riota 5622  df-ov 5669  df-oprab 5670  df-mpt2 5671  df-sub 7709

This theorem is referenced by:  addsubass  7746  npncan  7757  nppcan  7758  nnpcan  7759  subcan2  7761  nnncan  7771  npcand  7851  nn1suc  8495  zlem1lt  8860  zltlem1  8861  peano5uzti  8908  nummac  8975  uzp1  9106  peano2uzr  9127  fz01en  9521  fzsuc2  9547  fseq1m1p1  9563  fzoss2  9637  fzoaddel2  9658  fzosplitsnm1  9674  fzosplitprm1  9699  modfzo0difsn  9856  iseqm1  9942  seq3m1  9943  monoord2  9959  isermono  9960  expm1t  10037  expubnd  10066  bcm1k  10222  bcn2  10226  hashfzo  10284  iseqcoll  10301  shftlem  10304  shftfvalg  10306  shftfval  10309  iserex  10781  serf0  10795  fsumm1  10864  mptfzshft  10890  binomlem  10931  binom1dif  10935  isumsplit  10939  dvdssub2  11170