Theorem pncan3d 11571

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 11465	. 2 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 + (𝐵 − 𝐴)) = 𝐵)
4	1, 2, 3	syl2anc 585	1 ⊢ (𝜑 → (𝐴 + (𝐵 − 𝐴)) = 𝐵)

Syntax hints:   → wi 4   = wceq 1542   ∈ wcel 2107  (class class class)co 7406  ℂcc 11105   + caddc 11110   − cmin 11441

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2704  ax-sep 5299  ax-nul 5306  ax-pow 5363  ax-pr 5427  ax-un 7722  ax-resscn 11164  ax-1cn 11165  ax-icn 11166  ax-addcl 11167  ax-addrcl 11168  ax-mulcl 11169  ax-mulrcl 11170  ax-mulcom 11171  ax-addass 11172  ax-mulass 11173  ax-distr 11174  ax-i2m1 11175  ax-1ne0 11176  ax-1rid 11177  ax-rnegex 11178  ax-rrecex 11179  ax-cnre 11180  ax-pre-lttri 11181  ax-pre-lttrn 11182  ax-pre-ltadd 11183

This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3or 1089  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2535  df-eu 2564  df-clab 2711  df-cleq 2725  df-clel 2811  df-nfc 2886  df-ne 2942  df-nel 3048  df-ral 3063  df-rex 3072  df-reu 3378  df-rab 3434  df-v 3477  df-sbc 3778  df-csb 3894  df-dif 3951  df-un 3953  df-in 3955  df-ss 3965  df-nul 4323  df-if 4529  df-pw 4604  df-sn 4629  df-pr 4631  df-op 4635  df-uni 4909  df-br 5149  df-opab 5211  df-mpt 5232  df-id 5574  df-po 5588  df-so 5589  df-xp 5682  df-rel 5683  df-cnv 5684  df-co 5685  df-dm 5686  df-rn 5687  df-res 5688  df-ima 5689  df-iota 6493  df-fun 6543  df-fn 6544  df-f 6545  df-f1 6546  df-fo 6547  df-f1o 6548  df-fv 6549  df-riota 7362  df-ov 7409  df-oprab 7410  df-mpo 7411  df-er 8700  df-en 8937  df-dom 8938  df-sdom 8939  df-pnf 11247  df-mnf 11248  df-ltxr 11250  df-sub 11443

This theorem is referenced by:  xralrple  13181  quoremz  13817  quoremnn0ALT  13819  intfrac2  13820  intfrac  13848  2cshwcshw  14773  isercoll2  15612  iseralt  15628  mertenslem1  15827  fprodser  15890  risefacfac  15976  fallfacfwd  15977  eflt  16057  efival  16092  bitsmod  16374  bitsinv1lem  16379  odzdvds  16725  modprm0  16735  pcaddlem  16818  vdwapun  16904  vdwlem12  16922  odmodnn0  19403  mndodconglem  19404  mhpmulcl  21684  minveclem4  24941  ivthlem2  24961  dvn2bss  25439  ftc2  25553  mdegmullem  25588  plymullem1  25720  dvtaylp  25874  dvntaylp  25875  dvntaylp0  25876  taylthlem1  25877  ulmbdd  25902  affineequiv  26318  mcubic  26342  quart1lem  26350  quart1  26351  asinsin  26387  birthdaylem2  26447  emcllem6  26495  perfectlem2  26723  lgseisenlem4  26871  lgsquadlem1  26873  addsqnreup  26936  dchrisumlem1  26982  dchrvmasum2if  26990  dchrisum0lem1  27009  selberg3  27052  axsegconlem10  28174  smcnlem  29938  swrdrn3  32107  cycpmco2lem6  32278  oddpwdc  33342  revpfxsfxrev  34095  itg2addnclem3  36530  ftc2nc  36559  dvrelogpow2b  40922  sticksstones10  40960  sticksstones12a  40962  metakunt16  40989  metakunt20  40993  frlmvscadiccat  41078  dffltz  41373  fltnltalem  41401  fltnlta  41402  fzisoeu  43997  lptre2pt  44343  0ellimcdiv  44352  climleltrp  44379  ioodvbdlimc1lem2  44635  dvnprodlem1  44649  itgsinexp  44658  itgsbtaddcnst  44685  dirkertrigeqlem2  44802  fourierdlem4  44814  fourierdlem13  44823  fourierdlem26  44836  fourierdlem41  44851  fourierdlem42  44852  fourierdlem50  44859  fourierdlem60  44869  fourierdlem61  44870  fourierdlem74  44883  fourierdlem75  44884  fourierdlem76  44885  fourierdlem84  44893  fourierdlem89  44898  fourierdlem90  44899  fourierdlem91  44900  fourierdlem93  44902  fourierdlem101  44910  fourierdlem107  44916  fourierdlem111  44920  fourierdlem112  44921  fouriersw  44934  smfaddlem1  45466  sigarcol  45567  perfectALTVlem2  46377  nnpw2pmod  47223  rrx2vlinest  47381  itsclc0xyqsolr  47409