Theorem subnegd 11594

Description: Relationship between subtraction and negative. (Contributed by Mario Carneiro, 27-May-2016.)

Hypotheses

Ref	Expression
negidd.1	⊢ (𝜑 → 𝐴 ∈ ℂ)
pncand.2	⊢ (𝜑 → 𝐵 ∈ ℂ)

Assertion

Ref	Expression
subnegd	⊢ (𝜑 → (𝐴 − -𝐵) = (𝐴 + 𝐵))

Proof of Theorem subnegd

Step	Hyp	Ref	Expression
1		negidd.1	. 2 ⊢ (𝜑 → 𝐴 ∈ ℂ)
2		pncand.2	. 2 ⊢ (𝜑 → 𝐵 ∈ ℂ)
3		subneg 11525	. 2 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 − -𝐵) = (𝐴 + 𝐵))
4	1, 2, 3	syl2anc 584	1 ⊢ (𝜑 → (𝐴 − -𝐵) = (𝐴 + 𝐵))

Syntax hints:   → wi 4   = wceq 1539   ∈ wcel 2107  (class class class)co 7400  ℂcc 11120   + caddc 11125   − cmin 11459  -cneg 11460

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-8 2109  ax-9 2117  ax-10 2140  ax-11 2156  ax-12 2176  ax-ext 2706  ax-sep 5264  ax-nul 5274  ax-pow 5333  ax-pr 5400  ax-un 7724  ax-resscn 11179  ax-1cn 11180  ax-icn 11181  ax-addcl 11182  ax-addrcl 11183  ax-mulcl 11184  ax-mulrcl 11185  ax-mulcom 11186  ax-addass 11187  ax-mulass 11188  ax-distr 11189  ax-i2m1 11190  ax-1ne0 11191  ax-1rid 11192  ax-rnegex 11193  ax-rrecex 11194  ax-cnre 11195  ax-pre-lttri 11196  ax-pre-lttrn 11197  ax-pre-ltadd 11198

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1779  df-nf 1783  df-sb 2064  df-mo 2538  df-eu 2567  df-clab 2713  df-cleq 2726  df-clel 2808  df-nfc 2884  df-ne 2932  df-nel 3036  df-ral 3051  df-rex 3060  df-reu 3358  df-rab 3414  df-v 3459  df-sbc 3764  df-csb 3873  df-dif 3927  df-un 3929  df-in 3931  df-ss 3941  df-nul 4307  df-if 4499  df-pw 4575  df-sn 4600  df-pr 4602  df-op 4606  df-uni 4882  df-br 5118  df-opab 5180  df-mpt 5200  df-id 5546  df-po 5559  df-so 5560  df-xp 5658  df-rel 5659  df-cnv 5660  df-co 5661  df-dm 5662  df-rn 5663  df-res 5664  df-ima 5665  df-iota 6481  df-fun 6530  df-fn 6531  df-f 6532  df-f1 6533  df-fo 6534  df-f1o 6535  df-fv 6536  df-riota 7357  df-ov 7403  df-oprab 7404  df-mpo 7405  df-er 8714  df-en 8955  df-dom 8956  df-sdom 8957  df-pnf 11264  df-mnf 11265  df-ltxr 11267  df-sub 11461  df-neg 11462

This theorem is referenced by:  possumd  11855  dfceil2  13846  addmodlteq  13954  ipcnval  15151  fallfacfwd  16041  cossub  16174  znunit  21511  cphsqrtcl2  25125  ulmshft  26338  ptolemy  26443  efeq1  26475  quad2  26787  dcubic2  26792  dcubic  26794  mcubic  26795  dquartlem1  26799  quart  26809  asinlem  26816  asinlem2  26817  sinasin  26837  asinsin  26840  atandmtan  26868  atantan  26871  lgamgulmlem2  26978  lgambdd  26985  lgamucov  26986  lgseisenlem2  27325  rpvmasum2  27461  chpdifbndlem1  27502  pntrsumo1  27514  pntrlog2bndlem4  27529  nvabs  30587  pythagreim  32659  constrreinvcl  33741  breprexplemc  34593  logdivsqrle  34611  irrdiff  37273  poimirlem29  37602  areacirc  37666  posbezout  42042  acongrep  42936  acongeq  42939  jm2.25  42955  jm2.26lem3  42957  sqrtcvallem4  43595  sqrtcval  43597  radcnvrat  44271  dvradcnv2  44304  binomcxplemnotnn0  44313  fperiodmul  45267  itgsincmulx  45939  fourierdlem103  46174  fourierdlem109  46180  fourierdlem111  46182  sqwvfoura  46193  etransclem46  46245  hoicvrrex  46521  sigarms  46821  fmtnorec3  47488  2pwp1prm  47529  eenglngeehlnmlem1  48611  itsclc0yqsol  48638