Theorem pncan3d 11497

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

Syntax hints:   → wi 4   = wceq 1542   ∈ wcel 2114  (class class class)co 7358  ℂcc 11025   + caddc 11030   − cmin 11366

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2709  ax-sep 5231  ax-nul 5241  ax-pow 5300  ax-pr 5368  ax-un 7680  ax-resscn 11084  ax-1cn 11085  ax-icn 11086  ax-addcl 11087  ax-addrcl 11088  ax-mulcl 11089  ax-mulrcl 11090  ax-mulcom 11091  ax-addass 11092  ax-mulass 11093  ax-distr 11094  ax-i2m1 11095  ax-1ne0 11096  ax-1rid 11097  ax-rnegex 11098  ax-rrecex 11099  ax-cnre 11100  ax-pre-lttri 11101  ax-pre-lttrn 11102  ax-pre-ltadd 11103

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2540  df-eu 2570  df-clab 2716  df-cleq 2729  df-clel 2812  df-nfc 2886  df-ne 2934  df-nel 3038  df-ral 3053  df-rex 3063  df-reu 3344  df-rab 3391  df-v 3432  df-sbc 3730  df-csb 3839  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-nul 4275  df-if 4468  df-pw 4544  df-sn 4569  df-pr 4571  df-op 4575  df-uni 4852  df-br 5087  df-opab 5149  df-mpt 5168  df-id 5517  df-po 5530  df-so 5531  df-xp 5628  df-rel 5629  df-cnv 5630  df-co 5631  df-dm 5632  df-rn 5633  df-res 5634  df-ima 5635  df-iota 6446  df-fun 6492  df-fn 6493  df-f 6494  df-f1 6495  df-fo 6496  df-f1o 6497  df-fv 6498  df-riota 7315  df-ov 7361  df-oprab 7362  df-mpo 7363  df-er 8634  df-en 8885  df-dom 8886  df-sdom 8887  df-pnf 11170  df-mnf 11171  df-ltxr 11173  df-sub 11368

This theorem is referenced by:  xralrple  13146  quoremz  13803  quoremnn0ALT  13805  intfrac2  13806  intfrac  13834  2cshwcshw  14776  isercoll2  15620  iseralt  15636  mertenslem1  15838  fprodser  15903  risefacfac  15989  fallfacfwd  15990  eflt  16073  efival  16108  bitsmod  16394  bitsinv1lem  16399  odzdvds  16755  modprm0  16765  pcaddlem  16848  vdwapun  16934  vdwlem12  16952  odmodnn0  19504  mndodconglem  19505  pzriprnglem10  21478  mhpmulcl  22123  psdmul  22140  minveclem4  25407  ivthlem2  25427  dvn2bss  25905  ftc2  26019  mdegmullem  26051  plymullem1  26187  dvtaylp  26345  dvntaylp  26346  dvntaylp0  26347  taylthlem1  26348  ulmbdd  26374  affineequiv  26798  mcubic  26822  quart1lem  26830  quart1  26831  asinsin  26867  birthdaylem2  26927  emcllem6  26976  perfectlem2  27205  lgseisenlem4  27353  lgsquadlem1  27355  addsqnreup  27418  dchrisumlem1  27464  dchrvmasum2if  27472  dchrisum0lem1  27491  selberg3  27534  axsegconlem10  29007  smcnlem  30781  swrdrn3  33028  cycpmco2lem6  33205  constrremulcl  33925  constrreinvcl  33930  oddpwdc  34512  revpfxsfxrev  35312  itg2addnclem3  37998  ftc2nc  38027  dvrelogpow2b  42511  hashscontpow1  42564  sticksstones10  42598  sticksstones12a  42600  frlmvscadiccat  42955  dffltz  43071  fltnltalem  43099  fltnlta  43100  fzisoeu  45741  lptre2pt  46076  0ellimcdiv  46085  climleltrp  46112  ioodvbdlimc1lem2  46368  dvnprodlem1  46382  itgsinexp  46391  itgsbtaddcnst  46418  dirkertrigeqlem2  46535  fourierdlem4  46547  fourierdlem13  46556  fourierdlem26  46569  fourierdlem41  46584  fourierdlem42  46585  fourierdlem50  46592  fourierdlem60  46602  fourierdlem61  46603  fourierdlem74  46616  fourierdlem75  46617  fourierdlem76  46618  fourierdlem84  46626  fourierdlem89  46631  fourierdlem90  46632  fourierdlem91  46633  fourierdlem93  46635  fourierdlem101  46643  fourierdlem107  46649  fourierdlem111  46653  fourierdlem112  46654  fouriersw  46667  smfaddlem1  47199  sigarcol  47300  perfectALTVlem2  48200  nnpw2pmod  49061  rrx2vlinest  49219  itsclc0xyqsolr  49247