Theorem pncan2d 11495

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

Hypotheses

Ref	Expression
negidd.1	⊢ (𝜑 → 𝐴 ∈ ℂ)
pncand.2	⊢ (𝜑 → 𝐵 ∈ ℂ)

Assertion

Ref	Expression
pncan2d	⊢ (𝜑 → ((𝐴 + 𝐵) − 𝐴) = 𝐵)

Proof of Theorem pncan2d

Step	Hyp	Ref	Expression
1		negidd.1	. 2 ⊢ (𝜑 → 𝐴 ∈ ℂ)
2		pncand.2	. 2 ⊢ (𝜑 → 𝐵 ∈ ℂ)
3		pncan2 11388	. 2 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((𝐴 + 𝐵) − 𝐴) = 𝐵)
4	1, 2, 3	syl2anc 584	1 ⊢ (𝜑 → ((𝐴 + 𝐵) − 𝐴) = 𝐵)

Syntax hints:   → wi 4   = wceq 1540   ∈ wcel 2109  (class class class)co 7353  ℂcc 11026   + caddc 11031   − cmin 11365

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 5238  ax-nul 5248  ax-pow 5307  ax-pr 5374  ax-un 7675  ax-resscn 11085  ax-1cn 11086  ax-icn 11087  ax-addcl 11088  ax-addrcl 11089  ax-mulcl 11090  ax-mulrcl 11091  ax-mulcom 11092  ax-addass 11093  ax-mulass 11094  ax-distr 11095  ax-i2m1 11096  ax-1ne0 11097  ax-1rid 11098  ax-rnegex 11099  ax-rrecex 11100  ax-cnre 11101  ax-pre-lttri 11102  ax-pre-lttrn 11103  ax-pre-ltadd 11104

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 3346  df-rab 3397  df-v 3440  df-sbc 3745  df-csb 3854  df-dif 3908  df-un 3910  df-in 3912  df-ss 3922  df-nul 4287  df-if 4479  df-pw 4555  df-sn 4580  df-pr 4582  df-op 4586  df-uni 4862  df-br 5096  df-opab 5158  df-mpt 5177  df-id 5518  df-po 5531  df-so 5532  df-xp 5629  df-rel 5630  df-cnv 5631  df-co 5632  df-dm 5633  df-rn 5634  df-res 5635  df-ima 5636  df-iota 6442  df-fun 6488  df-fn 6489  df-f 6490  df-f1 6491  df-fo 6492  df-f1o 6493  df-fv 6494  df-riota 7310  df-ov 7356  df-oprab 7357  df-mpo 7358  df-er 8632  df-en 8880  df-dom 8881  df-sdom 8882  df-pnf 11170  df-mnf 11171  df-ltxr 11173  df-sub 11367

This theorem is referenced by:  xov1plusxeqvd  13419  fzocatel  13650  expaddzlem  14030  hashf1lem2  14381  imval2  15076  clim2ser  15580  serf0  15606  fsumrev2  15707  geolim2  15796  mertenslem2  15810  bpolydiflem  15979  addmulmodb  16194  dvdsadd2b  16235  sadadd3  16390  mulgdirlem  19002  cnsubrg  21352  coe1tmmul2fv  22180  coe1pwmulfv  22182  reperflem  24723  reconnlem2  24732  ioorcl2  25489  uniioombllem3  25502  lhop1lem  25934  dvfsumabs  25945  ftc1lem1  25958  itgparts  25970  itgsubstlem  25971  coe1mul3  26020  coemulhi  26175  abelthlem6  26362  efif1olem4  26470  efopn  26583  dcubic2  26770  birthdaylem2  26878  lgamcvg2  26981  chtdif  27084  lgsquadlem1  27307  2sqmod  27363  dchrisumlem1  27416  dchrisumlem2  27417  dchrisum0lem1b  27442  pntrlog2bndlem1  27504  pntrlog2bndlem2  27505  axsegconlem9  28888  axpaschlem  28903  cycpmco2lem3  33083  cycpmco2lem4  33084  cycpmco2lem5  33085  cycpmco2lem6  33086  cycpmco2  33088  archiabllem1a  33143  nn0constr  33727  constraddcl  33728  constrreinvcl  33738  probdif  34387  ballotlemsi  34482  knoppndvlem14  36498  knoppndvlem16  36500  bj-bary1lem1  37284  ftc1anc  37680  sticksstones12  42131  bcle2d  42152  readdrcl2d  42246  lsubrotld  42250  sumcubes  42286  jm2.27c  42980  jm3.1lem2  42991  radcnvrat  44287  binomcxplemdvbinom  44326  binomcxplemnotnn0  44329  mccllem  45579  ioodvbdlimc1lem2  45914  stirlinglem5  46060  fourierdlem7  46096  fourierdlem19  46108  fourierdlem26  46115  fourierdlem42  46131  fourierdlem63  46151  fourierdlem65  46153  fourierdlem79  46167  fourierdlem89  46177  fourierdlem90  46178  fourierdlem91  46179  fourierdlem101  46189  fourierdlem112  46200  qndenserrnbllem  46276  submodaddmod  47326  zplusmodne  47328