Theorem negsubdi2d 11558

Description: Distribution of negative over subtraction. (Contributed by Mario Carneiro, 27-May-2016.)

Hypotheses

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

Assertion

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

Proof of Theorem negsubdi2d

Step	Hyp	Ref	Expression
1		negidd.1	. 2 ⊢ (𝜑 → 𝐴 ∈ ℂ)
2		pncand.2	. 2 ⊢ (𝜑 → 𝐵 ∈ ℂ)
3		negsubdi2 11490	. 2 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → -(𝐴 − 𝐵) = (𝐵 − 𝐴))
4	1, 2, 3	syl2anc 593	1 ⊢ (𝜑 → -(𝐴 − 𝐵) = (𝐵 − 𝐴))

Syntax hints:   → wi 4   = wceq 1560   ∈ wcel 2142  (class class class)co 7396  ℂcc 11071   − cmin 11414  -cneg 11415

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1815  ax-4 1829  ax-5 1930  ax-6 1987  ax-7 2028  ax-8 2144  ax-9 2152  ax-10 2175  ax-11 2191  ax-12 2212  ax-ext 2734  ax-sep 5246  ax-nul 5256  ax-pow 5322  ax-pr 5390  ax-un 7718  ax-resscn 11130  ax-1cn 11131  ax-icn 11132  ax-addcl 11133  ax-addrcl 11134  ax-mulcl 11135  ax-mulrcl 11136  ax-mulcom 11137  ax-addass 11138  ax-mulass 11139  ax-distr 11140  ax-i2m1 11141  ax-1ne0 11142  ax-1rid 11143  ax-rnegex 11144  ax-rrecex 11145  ax-cnre 11146  ax-pre-lttri 11147  ax-pre-lttrn 11148  ax-pre-ltadd 11149

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-3or 1099  df-3an 1100  df-tru 1563  df-fal 1573  df-ex 1800  df-nf 1804  df-sb 2091  df-mo 2566  df-eu 2596  df-clab 2741  df-cleq 2754  df-clel 2837  df-nfc 2911  df-ne 2958  df-nel 3062  df-ral 3077  df-rex 3087  df-reu 3368  df-rab 3415  df-v 3456  df-sbc 3745  df-csb 3853  df-dif 3907  df-un 3909  df-in 3911  df-ss 3921  df-nul 4286  df-if 4481  df-pw 4557  df-sn 4583  df-pr 4585  df-op 4589  df-uni 4866  df-br 5101  df-opab 5163  df-mpt 5182  df-id 5542  df-po 5555  df-so 5556  df-xp 5653  df-rel 5654  df-cnv 5655  df-co 5656  df-dm 5657  df-rn 5658  df-res 5659  df-ima 5660  df-iota 6477  df-fun 6523  df-fn 6524  df-f 6525  df-f1 6526  df-fo 6527  df-f1o 6528  df-fv 6529  df-riota 7353  df-ov 7399  df-oprab 7400  df-mpo 7401  df-er 8678  df-en 8928  df-dom 8929  df-sdom 8930  df-pnf 11218  df-mnf 11219  df-ltxr 11221  df-sub 11416  df-neg 11417

This theorem is referenced by:  cjneg  15174  icodiamlt  15465  geo2sum2  15904  bpoly3  16088  sinneg  16178  sinhval  16186  vitalilem1  25670  vitalilem2  25671  itgneg  25866  dvrec  26017  dvferm2lem  26048  dvfsumge  26084  dvfsumlem2  26089  dvfsum2  26096  ftc1lem5  26102  ftc2ditg  26108  plyeq0lem  26270  efif1olem2  26608  ang180  26879  isosctrlem3  26885  isosctr  26886  affineequiv3  26890  angpieqvdlem  26893  chordthmlem  26897  mcubic  26912  quart1lem  26920  quartlem1  26922  atanneg  26972  atancj  26975  efiatan  26977  atanlogsub  26981  efiatan2  26982  2efiatan  26983  atantan  26988  atanbndlem  26990  pntrsumo1  27629  pntrlog2bndlem2  27642  pntrlog2bndlem4  27644  pntibndlem2  27655  brbtwn2  29106  colinearalglem4  29110  axsegconlem9  29126  dipcj  30917  bcm1n  32997  constrrtcc  34032  constrrecl  34066  cos9thpiminplylem1  34079  signsplypnf  34844  fsum2dsub  34901  dnibndlem11  36926  irrdifflemf  37817  itg2addnclem3  38172  itg2gt0cn  38174  aks6d1c5lem1  42753  sinpim  42959  cospim  42960  congsym  43545  cvgdvgrat  44889  negsubdi3d  45872  lptre2pt  46214  liminflimsupclim  46381  stoweidlem13  46587  dirkertrigeqlem2  46673  fourierdlem26  46707  fourierdlem89  46769  fourierdlem90  46770  fourierdlem91  46771  fourierdlem107  46787  etransclem23  46831  sharhght  47439  sigaradd  47440  cevathlem2  47442  difmodm1lt  47959  fmtnorec3  48157  1subrec1sub  49327  eenglngeehlnmlem1  49359  eenglngeehlnmlem2  49360  rrx2linest  49364  rrx2linest2  49366  line2  49374  itsclinecirc0b  49396