MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  pncan3d Structured version   Visualization version   GIF version

Theorem pncan3d 10476
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
StepHypRef Expression
1 negidd.1 . 2 (𝜑𝐴 ∈ ℂ)
2 pncand.2 . 2 (𝜑𝐵 ∈ ℂ)
3 pncan3 10370 . 2 ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 + (𝐵𝐴)) = 𝐵)
41, 2, 3syl2anc 696 1 (𝜑 → (𝐴 + (𝐵𝐴)) = 𝐵)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1564  wcel 2071  (class class class)co 6733  cc 10015   + caddc 10020  cmin 10347
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1818  ax-5 1920  ax-6 1986  ax-7 2022  ax-8 2073  ax-9 2080  ax-10 2100  ax-11 2115  ax-12 2128  ax-13 2323  ax-ext 2672  ax-sep 4857  ax-nul 4865  ax-pow 4916  ax-pr 4979  ax-un 7034  ax-resscn 10074  ax-1cn 10075  ax-icn 10076  ax-addcl 10077  ax-addrcl 10078  ax-mulcl 10079  ax-mulrcl 10080  ax-mulcom 10081  ax-addass 10082  ax-mulass 10083  ax-distr 10084  ax-i2m1 10085  ax-1ne0 10086  ax-1rid 10087  ax-rnegex 10088  ax-rrecex 10089  ax-cnre 10090  ax-pre-lttri 10091  ax-pre-lttrn 10092  ax-pre-ltadd 10093
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3or 1073  df-3an 1074  df-tru 1567  df-ex 1786  df-nf 1791  df-sb 1979  df-eu 2543  df-mo 2544  df-clab 2679  df-cleq 2685  df-clel 2688  df-nfc 2823  df-ne 2865  df-nel 2968  df-ral 2987  df-rex 2988  df-reu 2989  df-rab 2991  df-v 3274  df-sbc 3510  df-csb 3608  df-dif 3651  df-un 3653  df-in 3655  df-ss 3662  df-nul 3992  df-if 4163  df-pw 4236  df-sn 4254  df-pr 4256  df-op 4260  df-uni 4513  df-br 4729  df-opab 4789  df-mpt 4806  df-id 5096  df-po 5107  df-so 5108  df-xp 5192  df-rel 5193  df-cnv 5194  df-co 5195  df-dm 5196  df-rn 5197  df-res 5198  df-ima 5199  df-iota 5932  df-fun 5971  df-fn 5972  df-f 5973  df-f1 5974  df-fo 5975  df-f1o 5976  df-fv 5977  df-riota 6694  df-ov 6736  df-oprab 6737  df-mpt2 6738  df-er 7830  df-en 8041  df-dom 8042  df-sdom 8043  df-pnf 10157  df-mnf 10158  df-ltxr 10160  df-sub 10349
This theorem is referenced by:  xralrple  12118  quoremz  12737  quoremnn0ALT  12739  intfrac2  12740  intfrac  12768  2cshwcshw  13660  isercoll2  14487  iseralt  14503  mertenslem1  14704  fprodser  14767  risefacfac  14854  fallfacfwd  14855  eflt  14935  efival  14970  bitsmod  15249  bitsinv1lem  15254  odzdvds  15591  modprm0  15601  pcaddlem  15683  vdwapun  15769  vdwlem12  15787  odmodnn0  18048  mndodconglem  18049  minveclem4  23292  ivthlem2  23310  dvn2bss  23781  ftc2  23895  mdegmullem  23926  plymullem1  24058  dvtaylp  24212  dvntaylp  24213  dvntaylp0  24214  taylthlem1  24215  ulmbdd  24240  affineequiv  24641  mcubic  24662  quart1lem  24670  quart1  24671  asinsin  24707  birthdaylem2  24767  emcllem6  24815  perfectlem2  25043  lgseisenlem4  25191  lgsquadlem1  25193  dchrisumlem1  25266  dchrvmasum2if  25274  dchrisum0lem1  25293  selberg3  25336  axsegconlem10  25894  smcnlem  27750  oddpwdc  30614  itg2addnclem3  33663  ftc2nc  33694  fzisoeu  39898  lptre2pt  40260  0ellimcdiv  40269  climleltrp  40296  ioodvbdlimc1lem2  40535  dvnprodlem1  40549  itgsinexp  40558  itgsbtaddcnst  40586  dirkertrigeqlem2  40704  fourierdlem4  40716  fourierdlem13  40725  fourierdlem26  40738  fourierdlem41  40753  fourierdlem42  40754  fourierdlem50  40761  fourierdlem60  40771  fourierdlem61  40772  fourierdlem74  40785  fourierdlem75  40786  fourierdlem76  40787  fourierdlem84  40795  fourierdlem89  40800  fourierdlem90  40801  fourierdlem91  40802  fourierdlem93  40804  fourierdlem101  40812  fourierdlem107  40818  fourierdlem111  40822  fourierdlem112  40823  fouriersw  40836  smfaddlem1  41362  sigarcol  41444  ccatpfx  41804  perfectALTVlem2  42026  nnpw2pmod  42772
  Copyright terms: Public domain W3C validator