Theorem addsubassd 11209

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

Hypotheses

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

Assertion

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

Proof of Theorem addsubassd

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

Syntax hints:   → wi 4   = wceq 1543   ∈ wcel 2110  (class class class)co 7213  ℂcc 10727   + caddc 10732   − cmin 11062

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 2112  ax-9 2120  ax-10 2141  ax-11 2158  ax-12 2175  ax-ext 2708  ax-sep 5192  ax-nul 5199  ax-pow 5258  ax-pr 5322  ax-un 7523  ax-resscn 10786  ax-1cn 10787  ax-icn 10788  ax-addcl 10789  ax-addrcl 10790  ax-mulcl 10791  ax-mulrcl 10792  ax-mulcom 10793  ax-addass 10794  ax-mulass 10795  ax-distr 10796  ax-i2m1 10797  ax-1ne0 10798  ax-1rid 10799  ax-rnegex 10800  ax-rrecex 10801  ax-cnre 10802  ax-pre-lttri 10803  ax-pre-lttrn 10804  ax-pre-ltadd 10805

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 2071  df-mo 2539  df-eu 2568  df-clab 2715  df-cleq 2729  df-clel 2816  df-nfc 2886  df-ne 2941  df-nel 3047  df-ral 3066  df-rex 3067  df-reu 3068  df-rab 3070  df-v 3410  df-sbc 3695  df-csb 3812  df-dif 3869  df-un 3871  df-in 3873  df-ss 3883  df-nul 4238  df-if 4440  df-pw 4515  df-sn 4542  df-pr 4544  df-op 4548  df-uni 4820  df-br 5054  df-opab 5116  df-mpt 5136  df-id 5455  df-po 5468  df-so 5469  df-xp 5557  df-rel 5558  df-cnv 5559  df-co 5560  df-dm 5561  df-rn 5562  df-res 5563  df-ima 5564  df-iota 6338  df-fun 6382  df-fn 6383  df-f 6384  df-f1 6385  df-fo 6386  df-f1o 6387  df-fv 6388  df-riota 7170  df-ov 7216  df-oprab 7217  df-mpo 7218  df-er 8391  df-en 8627  df-dom 8628  df-sdom 8629  df-pnf 10869  df-mnf 10870  df-ltxr 10872  df-sub 11064

This theorem is referenced by:  assraddsubd  11246  mulsubdivbinom2  13828  hashun3  13951  swrdccatin2  14294  bpoly4  15621  gsumsgrpccat  18266  gsumccatOLD  18267  mndodconglem  18933  efgredleme  19133  ovollb2lem  24385  ply1divex  25034  tanarg  25507  affineequiv  25706  chordthmlem4  25718  heron  25721  dquartlem2  25735  quart  25744  bposlem9  26173  2lgslem3b  26278  2lgslem3c  26279  2lgslem3d  26280  dchrisum0re  26394  mulog2sumlem1  26415  selberglem2  26427  selberg4  26442  selbergr  26449  selberg3r  26450  selberg34r  26452  brbtwn2  26996  ax5seglem2  27020  wwlksnextwrd  27981  wwlksnextinj  27983  clwwlkccatlem  28072  ex-ind-dvds  28544  lt2addrd  30794  cycpmco2lem3  31114  cycpmco2lem4  31115  cycpmco2lem5  31116  cycpmco2lem6  31117  cycpmco2  31119  archirngz  31162  fibp1  32080  dnibndlem10  34404  bj-bary1lem  35215  lcmineqlem22  39792  sticksstones10  39833  sticksstones12a  39835  3cubeslem2  40210  acongeq  40508  jm3.1lem2  40543  inductionexd  41442  fzisoeu  42512  sumnnodd  42846  stoweidlem26  43242  wallispilem4  43284  wallispi2lem1  43287  wallispi2lem2  43288  fourierdlem26  43349  fourierdlem41  43364  fourierdlem42  43365  fourierdlem48  43370  fourierdlem63  43385  fourierdlem107  43429  smfmullem1  43997  fmtnorec2lem  44667  fmtnorec3  44673  lighneallem3  44732  bgoldbtbndlem2  44931  m1modmmod  45540  itscnhlc0yqe  45778  2itscplem1  45797  2itscplem3  45799