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

Theorem subsub4d 11249
Description: Law for double subtraction. (Contributed by Mario Carneiro, 27-May-2016.)
Hypotheses
Ref Expression
negidd.1 (𝜑𝐴 ∈ ℂ)
pncand.2 (𝜑𝐵 ∈ ℂ)
subaddd.3 (𝜑𝐶 ∈ ℂ)
Assertion
Ref Expression
subsub4d (𝜑 → ((𝐴𝐵) − 𝐶) = (𝐴 − (𝐵 + 𝐶)))

Proof of Theorem subsub4d
StepHypRef Expression
1 negidd.1 . 2 (𝜑𝐴 ∈ ℂ)
2 pncand.2 . 2 (𝜑𝐵 ∈ ℂ)
3 subaddd.3 . 2 (𝜑𝐶 ∈ ℂ)
4 subsub4 11140 . 2 ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → ((𝐴𝐵) − 𝐶) = (𝐴 − (𝐵 + 𝐶)))
51, 2, 3, 4syl3anc 1373 1 (𝜑 → ((𝐴𝐵) − 𝐶) = (𝐴 − (𝐵 + 𝐶)))
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1543  wcel 2112  (class class class)co 7234  cc 10756   + caddc 10761  cmin 11091
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2016  ax-8 2114  ax-9 2122  ax-10 2143  ax-11 2160  ax-12 2177  ax-ext 2710  ax-sep 5208  ax-nul 5215  ax-pow 5274  ax-pr 5338  ax-un 7544  ax-resscn 10815  ax-1cn 10816  ax-icn 10817  ax-addcl 10818  ax-addrcl 10819  ax-mulcl 10820  ax-mulrcl 10821  ax-mulcom 10822  ax-addass 10823  ax-mulass 10824  ax-distr 10825  ax-i2m1 10826  ax-1ne0 10827  ax-1rid 10828  ax-rnegex 10829  ax-rrecex 10830  ax-cnre 10831  ax-pre-lttri 10832  ax-pre-lttrn 10833  ax-pre-ltadd 10834
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 848  df-3or 1090  df-3an 1091  df-tru 1546  df-fal 1556  df-ex 1788  df-nf 1792  df-sb 2073  df-mo 2541  df-eu 2570  df-clab 2717  df-cleq 2731  df-clel 2818  df-nfc 2889  df-ne 2944  df-nel 3050  df-ral 3069  df-rex 3070  df-reu 3071  df-rab 3073  df-v 3425  df-sbc 3712  df-csb 3829  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-nul 4254  df-if 4456  df-pw 4531  df-sn 4558  df-pr 4560  df-op 4564  df-uni 4836  df-br 5070  df-opab 5132  df-mpt 5152  df-id 5471  df-po 5485  df-so 5486  df-xp 5574  df-rel 5575  df-cnv 5576  df-co 5577  df-dm 5578  df-rn 5579  df-res 5580  df-ima 5581  df-iota 6358  df-fun 6402  df-fn 6403  df-f 6404  df-f1 6405  df-fo 6406  df-f1o 6407  df-fv 6408  df-riota 7191  df-ov 7237  df-oprab 7238  df-mpo 7239  df-er 8414  df-en 8650  df-dom 8651  df-sdom 8652  df-pnf 10898  df-mnf 10899  df-ltxr 10901  df-sub 11093
This theorem is referenced by:  subaddmulsub  11324  sub1m1  12111  cnm2m1cnm3  12112  nn0n0n1ge2  12186  ubmelm1fzo  13367  hashf1  14055  ccatass  14177  isercolllem1  15260  caucvgrlem  15268  fsumparts  15402  incexclem  15432  arisum2  15457  pwdif  15464  bpolydiflem  15648  bpoly4  15653  sin01bnd  15778  cos01bnd  15779  vdwlem5  16570  vdwlem8  16573  efgredleme  19165  opnreen  23759  pjthlem1  24365  dveflem  24907  dvcvx  24948  dvfsumlem1  24954  efif1olem2  25463  tanarg  25538  dcubic1  25759  dquartlem1  25765  tanatan  25833  atans2  25845  harmonicbnd4  25924  basellem5  25998  logfaclbnd  26134  bcmono  26189  lgsquadlem1  26292  mulogsumlem  26443  mulog2sumlem1  26446  vmalogdivsum  26451  selbergr  26480  selberg3r  26481  brbtwn2  27027  colinearalglem1  27028  colinearalglem2  27029  colinearalglem4  27031  ax5seglem1  27050  clwlkclwwlklem2a4  28111  clwlkclwwlklem2a  28112  clwwlkext2edg  28170  clwwlknonex2lem1  28221  clwwlknonex2lem2  28222  pjhthlem1  29503  lt2addrd  30825  cycpmco2lem6  31148  ballotlemfp1  32201  signstfveq0  32299  revpfxsfxrev  32820  revwlk  32829  bcprod  33453  dnibndlem10  34437  lcmineqlem10  39816  sticksstones10  39874  sticksstones12a  39876  suplesup  42598  fperdvper  43180  dvnxpaek  43203  itgsinexp  43216  stoweidlem26  43287  stoweidlem34  43295  stirlinglem5  43339  fourierdlem26  43394  fourierdlem107  43474  vonioolem1  43938  dignn0flhalflem1  45679  itsclc0yqsollem1  45826  2itscplem3  45844
  Copyright terms: Public domain W3C validator