Theorem pncan3d 11496

Description: Subtraction and addition of equals. (Contributed by Mario Carneiro, 27-May-2016.)

Hypotheses

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

Assertion

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

Proof of Theorem pncan3d

Step	Hyp	Ref	Expression
1		negidd.1	. 2 ⊢ (𝜑 → 𝐴 ∈ ℂ)
2		pncand.2	. 2 ⊢ (𝜑 → 𝐵 ∈ ℂ)
3		pncan3 11389	. 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:  xralrple  13125  quoremz  13777  quoremnn0ALT  13779  intfrac2  13780  intfrac  13808  2cshwcshw  14750  isercoll2  15594  iseralt  15610  mertenslem1  15809  fprodser  15874  risefacfac  15960  fallfacfwd  15961  eflt  16044  efival  16079  bitsmod  16365  bitsinv1lem  16370  odzdvds  16725  modprm0  16735  pcaddlem  16818  vdwapun  16904  vdwlem12  16922  odmodnn0  19437  mndodconglem  19438  pzriprnglem10  21415  mhpmulcl  22052  psdmul  22069  minveclem4  25348  ivthlem2  25369  dvn2bss  25848  ftc2  25967  mdegmullem  25999  plymullem1  26135  dvtaylp  26294  dvntaylp  26295  dvntaylp0  26296  taylthlem1  26297  ulmbdd  26323  affineequiv  26749  mcubic  26773  quart1lem  26781  quart1  26782  asinsin  26818  birthdaylem2  26878  emcllem6  26927  perfectlem2  27157  lgseisenlem4  27305  lgsquadlem1  27307  addsqnreup  27370  dchrisumlem1  27416  dchrvmasum2if  27424  dchrisum0lem1  27443  selberg3  27486  axsegconlem10  28889  smcnlem  30659  swrdrn3  32910  cycpmco2lem6  33086  constrremulcl  33733  constrreinvcl  33738  oddpwdc  34321  revpfxsfxrev  35088  itg2addnclem3  37652  ftc2nc  37681  dvrelogpow2b  42041  hashscontpow1  42094  sticksstones10  42128  sticksstones12a  42130  frlmvscadiccat  42479  dffltz  42607  fltnltalem  42635  fltnlta  42636  fzisoeu  45282  lptre2pt  45622  0ellimcdiv  45631  climleltrp  45658  ioodvbdlimc1lem2  45914  dvnprodlem1  45928  itgsinexp  45937  itgsbtaddcnst  45964  dirkertrigeqlem2  46081  fourierdlem4  46093  fourierdlem13  46102  fourierdlem26  46115  fourierdlem41  46130  fourierdlem42  46131  fourierdlem50  46138  fourierdlem60  46148  fourierdlem61  46149  fourierdlem74  46162  fourierdlem75  46163  fourierdlem76  46164  fourierdlem84  46172  fourierdlem89  46177  fourierdlem90  46178  fourierdlem91  46179  fourierdlem93  46181  fourierdlem101  46189  fourierdlem107  46195  fourierdlem111  46199  fourierdlem112  46200  fouriersw  46213  smfaddlem1  46745  sigarcol  46846  perfectALTVlem2  47707  nnpw2pmod  48569  rrx2vlinest  48727  itsclc0xyqsolr  48755