Theorem addsubd 11588

Description: Law for subtraction and addition. (Contributed by Mario Carneiro, 27-May-2016.)

Hypotheses

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

Assertion

Ref	Expression
addsubd	⊢ (𝜑 → ((𝐴 + 𝐵) − 𝐶) = ((𝐴 − 𝐶) + 𝐵))

Proof of Theorem addsubd

Step	Hyp	Ref	Expression
1		negidd.1	. 2 ⊢ (𝜑 → 𝐴 ∈ ℂ)
2		pncand.2	. 2 ⊢ (𝜑 → 𝐵 ∈ ℂ)
3		subaddd.3	. 2 ⊢ (𝜑 → 𝐶 ∈ ℂ)
4		addsub 11467	. 2 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → ((𝐴 + 𝐵) − 𝐶) = ((𝐴 − 𝐶) + 𝐵))
5	1, 2, 3, 4	syl3anc 1371	1 ⊢ (𝜑 → ((𝐴 + 𝐵) − 𝐶) = ((𝐴 − 𝐶) + 𝐵))

Syntax hints:   → wi 4   = wceq 1541   ∈ wcel 2106  (class class class)co 7405  ℂcc 11104   + caddc 11109   − cmin 11440

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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2703  ax-sep 5298  ax-nul 5305  ax-pow 5362  ax-pr 5426  ax-un 7721  ax-resscn 11163  ax-1cn 11164  ax-icn 11165  ax-addcl 11166  ax-addrcl 11167  ax-mulcl 11168  ax-mulrcl 11169  ax-mulcom 11170  ax-addass 11171  ax-mulass 11172  ax-distr 11173  ax-i2m1 11174  ax-1ne0 11175  ax-1rid 11176  ax-rnegex 11177  ax-rrecex 11178  ax-cnre 11179  ax-pre-lttri 11180  ax-pre-lttrn 11181  ax-pre-ltadd 11182

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3or 1088  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2534  df-eu 2563  df-clab 2710  df-cleq 2724  df-clel 2810  df-nfc 2885  df-ne 2941  df-nel 3047  df-ral 3062  df-rex 3071  df-reu 3377  df-rab 3433  df-v 3476  df-sbc 3777  df-csb 3893  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-nul 4322  df-if 4528  df-pw 4603  df-sn 4628  df-pr 4630  df-op 4634  df-uni 4908  df-br 5148  df-opab 5210  df-mpt 5231  df-id 5573  df-po 5587  df-so 5588  df-xp 5681  df-rel 5682  df-cnv 5683  df-co 5684  df-dm 5685  df-rn 5686  df-res 5687  df-ima 5688  df-iota 6492  df-fun 6542  df-fn 6543  df-f 6544  df-f1 6545  df-fo 6546  df-f1o 6547  df-fv 6548  df-riota 7361  df-ov 7408  df-oprab 7409  df-mpo 7410  df-er 8699  df-en 8936  df-dom 8937  df-sdom 8938  df-pnf 11246  df-mnf 11247  df-ltxr 11249  df-sub 11442

This theorem is referenced by:  lesub2  11705  fzoshftral  13745  modadd1  13869  discr  14199  bcp1n  14272  bcpasc  14277  revccat  14712  crre  15057  isercoll2  15611  binomlem  15771  climcndslem1  15791  binomfallfaclem2  15980  pythagtriplem14  16757  vdwlem6  16915  gsumsgrpccat  18717  srgbinomlem3  20044  itgcnlem  25298  dvcvx  25528  dvfsumlem1  25534  dvfsumlem2  25535  plymullem1  25719  aaliou3lem2  25847  abelthlem2  25935  tangtx  26006  loglesqrt  26255  dcubic1  26339  quart1lem  26349  quartlem1  26351  basellem3  26576  basellem5  26578  chtub  26704  logfaclbnd  26714  bcp1ctr  26771  lgsquad2lem1  26876  2lgslem3b  26889  selberglem1  27037  selberg3  27051  selbergr  27060  selberg3r  27061  pntlemf  27097  pntlemo  27099  brbtwn2  28152  colinearalglem1  28153  colinearalglem2  28154  crctcsh  29067  clwwlkccatlem  29231  clwwlkel  29288  clwwlkwwlksb  29296  clwwlknonex2lem1  29349  ltesubnnd  32015  ballotlemfp1  33478  swrdwlk  34105  subfacp1lem6  34164  fwddifnp1  35125  gg-dvfsumlem2  35171  poimirlem25  36501  poimirlem26  36502  2np3bcnp1  40948  sticksstones12a  40961  jm2.24nn  41683  jm2.18  41712  jm2.25  41723  dvnmul  44645  fourierdlem4  44813  fourierdlem26  44835  fourierdlem42  44851  vonicclem1  45385  cnambpcma  45988  cnapbmcpd  45989  fmtnorec4  46203  ltsubaddb  47148  ltsubadd2b  47150  2itscplem3  47419