Theorem pncan3d 11543

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

Syntax hints:   → wi 4   = wceq 1540   ∈ wcel 2109  (class class class)co 7390  ℂcc 11073   + caddc 11078   − cmin 11412

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 2702  ax-sep 5254  ax-nul 5264  ax-pow 5323  ax-pr 5390  ax-un 7714  ax-resscn 11132  ax-1cn 11133  ax-icn 11134  ax-addcl 11135  ax-addrcl 11136  ax-mulcl 11137  ax-mulrcl 11138  ax-mulcom 11139  ax-addass 11140  ax-mulass 11141  ax-distr 11142  ax-i2m1 11143  ax-1ne0 11144  ax-1rid 11145  ax-rnegex 11146  ax-rrecex 11147  ax-cnre 11148  ax-pre-lttri 11149  ax-pre-lttrn 11150  ax-pre-ltadd 11151

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 2534  df-eu 2563  df-clab 2709  df-cleq 2722  df-clel 2804  df-nfc 2879  df-ne 2927  df-nel 3031  df-ral 3046  df-rex 3055  df-reu 3357  df-rab 3409  df-v 3452  df-sbc 3757  df-csb 3866  df-dif 3920  df-un 3922  df-in 3924  df-ss 3934  df-nul 4300  df-if 4492  df-pw 4568  df-sn 4593  df-pr 4595  df-op 4599  df-uni 4875  df-br 5111  df-opab 5173  df-mpt 5192  df-id 5536  df-po 5549  df-so 5550  df-xp 5647  df-rel 5648  df-cnv 5649  df-co 5650  df-dm 5651  df-rn 5652  df-res 5653  df-ima 5654  df-iota 6467  df-fun 6516  df-fn 6517  df-f 6518  df-f1 6519  df-fo 6520  df-f1o 6521  df-fv 6522  df-riota 7347  df-ov 7393  df-oprab 7394  df-mpo 7395  df-er 8674  df-en 8922  df-dom 8923  df-sdom 8924  df-pnf 11217  df-mnf 11218  df-ltxr 11220  df-sub 11414

This theorem is referenced by:  xralrple  13172  quoremz  13824  quoremnn0ALT  13826  intfrac2  13827  intfrac  13855  2cshwcshw  14798  isercoll2  15642  iseralt  15658  mertenslem1  15857  fprodser  15922  risefacfac  16008  fallfacfwd  16009  eflt  16092  efival  16127  bitsmod  16413  bitsinv1lem  16418  odzdvds  16773  modprm0  16783  pcaddlem  16866  vdwapun  16952  vdwlem12  16970  odmodnn0  19477  mndodconglem  19478  pzriprnglem10  21407  mhpmulcl  22043  psdmul  22060  minveclem4  25339  ivthlem2  25360  dvn2bss  25839  ftc2  25958  mdegmullem  25990  plymullem1  26126  dvtaylp  26285  dvntaylp  26286  dvntaylp0  26287  taylthlem1  26288  ulmbdd  26314  affineequiv  26740  mcubic  26764  quart1lem  26772  quart1  26773  asinsin  26809  birthdaylem2  26869  emcllem6  26918  perfectlem2  27148  lgseisenlem4  27296  lgsquadlem1  27298  addsqnreup  27361  dchrisumlem1  27407  dchrvmasum2if  27415  dchrisum0lem1  27434  selberg3  27477  axsegconlem10  28860  smcnlem  30633  swrdrn3  32884  cycpmco2lem6  33095  constrremulcl  33764  constrreinvcl  33769  oddpwdc  34352  revpfxsfxrev  35110  itg2addnclem3  37674  ftc2nc  37703  dvrelogpow2b  42063  hashscontpow1  42116  sticksstones10  42150  sticksstones12a  42152  frlmvscadiccat  42501  dffltz  42629  fltnltalem  42657  fltnlta  42658  fzisoeu  45305  lptre2pt  45645  0ellimcdiv  45654  climleltrp  45681  ioodvbdlimc1lem2  45937  dvnprodlem1  45951  itgsinexp  45960  itgsbtaddcnst  45987  dirkertrigeqlem2  46104  fourierdlem4  46116  fourierdlem13  46125  fourierdlem26  46138  fourierdlem41  46153  fourierdlem42  46154  fourierdlem50  46161  fourierdlem60  46171  fourierdlem61  46172  fourierdlem74  46185  fourierdlem75  46186  fourierdlem76  46187  fourierdlem84  46195  fourierdlem89  46200  fourierdlem90  46201  fourierdlem91  46202  fourierdlem93  46204  fourierdlem101  46212  fourierdlem107  46218  fourierdlem111  46222  fourierdlem112  46223  fouriersw  46236  smfaddlem1  46768  sigarcol  46869  perfectALTVlem2  47727  nnpw2pmod  48576  rrx2vlinest  48734  itsclc0xyqsolr  48762