Theorem addsubd 11622

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 11501	. 2 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → ((𝐴 + 𝐵) − 𝐶) = ((𝐴 − 𝐶) + 𝐵))
5	1, 2, 3, 4	syl3anc 1368	1 ⊢ (𝜑 → ((𝐴 + 𝐵) − 𝐶) = ((𝐴 − 𝐶) + 𝐵))

Syntax hints:   → wi 4   = wceq 1533   ∈ wcel 2098  (class class class)co 7417  ℂcc 11136   + caddc 11141   − cmin 11474

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-10 2129  ax-11 2146  ax-12 2166  ax-ext 2696  ax-sep 5299  ax-nul 5306  ax-pow 5364  ax-pr 5428  ax-un 7739  ax-resscn 11195  ax-1cn 11196  ax-icn 11197  ax-addcl 11198  ax-addrcl 11199  ax-mulcl 11200  ax-mulrcl 11201  ax-mulcom 11202  ax-addass 11203  ax-mulass 11204  ax-distr 11205  ax-i2m1 11206  ax-1ne0 11207  ax-1rid 11208  ax-rnegex 11209  ax-rrecex 11210  ax-cnre 11211  ax-pre-lttri 11212  ax-pre-lttrn 11213  ax-pre-ltadd 11214

This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-3or 1085  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-nf 1778  df-sb 2060  df-mo 2528  df-eu 2557  df-clab 2703  df-cleq 2717  df-clel 2802  df-nfc 2877  df-ne 2931  df-nel 3037  df-ral 3052  df-rex 3061  df-reu 3365  df-rab 3420  df-v 3465  df-sbc 3775  df-csb 3891  df-dif 3948  df-un 3950  df-in 3952  df-ss 3962  df-nul 4324  df-if 4530  df-pw 4605  df-sn 4630  df-pr 4632  df-op 4636  df-uni 4909  df-br 5149  df-opab 5211  df-mpt 5232  df-id 5575  df-po 5589  df-so 5590  df-xp 5683  df-rel 5684  df-cnv 5685  df-co 5686  df-dm 5687  df-rn 5688  df-res 5689  df-ima 5690  df-iota 6499  df-fun 6549  df-fn 6550  df-f 6551  df-f1 6552  df-fo 6553  df-f1o 6554  df-fv 6555  df-riota 7373  df-ov 7420  df-oprab 7421  df-mpo 7422  df-er 8723  df-en 8963  df-dom 8964  df-sdom 8965  df-pnf 11280  df-mnf 11281  df-ltxr 11283  df-sub 11476

This theorem is referenced by:  lesub2  11739  fzoshftral  13781  modadd1  13905  discr  14234  bcp1n  14307  bcpasc  14312  revccat  14748  crre  15093  isercoll2  15647  binomlem  15807  climcndslem1  15827  binomfallfaclem2  16016  pythagtriplem14  16796  vdwlem6  16954  gsumsgrpccat  18796  srgbinomlem3  20172  itgcnlem  25749  dvcvx  25983  dvfsumlem1  25990  dvfsumlem2  25991  dvfsumlem2OLD  25992  plymullem1  26178  aaliou3lem2  26308  abelthlem2  26399  tangtx  26470  loglesqrt  26723  dcubic1  26807  quart1lem  26817  quartlem1  26819  basellem3  27045  basellem5  27047  chtub  27175  logfaclbnd  27185  bcp1ctr  27242  lgsquad2lem1  27347  2lgslem3b  27360  selberglem1  27508  selberg3  27522  selbergr  27531  selberg3r  27532  pntlemf  27568  pntlemo  27570  brbtwn2  28772  colinearalglem1  28773  colinearalglem2  28774  crctcsh  29691  clwwlkccatlem  29855  clwwlkel  29912  clwwlkwwlksb  29920  clwwlknonex2lem1  29973  ltesubnnd  32642  ballotlemfp1  34181  swrdwlk  34806  subfacp1lem6  34865  fwddifnp1  35831  poimirlem25  37188  poimirlem26  37189  2np3bcnp1  41685  sticksstones12a  41698  jm2.24nn  42445  jm2.18  42474  jm2.25  42485  dvnmul  45394  fourierdlem4  45562  fourierdlem26  45584  fourierdlem42  45600  vonicclem1  46134  cnambpcma  46737  cnapbmcpd  46738  fmtnorec4  46952  ltsubaddb  47694  ltsubadd2b  47696  2itscplem3  47965