Theorem addid2d 11106

Description: 0 is a left identity for addition. (Contributed by Mario Carneiro, 27-May-2016.)

Hypothesis

Ref	Expression
muld.1	⊢ (𝜑 → 𝐴 ∈ ℂ)

Assertion

Ref	Expression
addid2d	⊢ (𝜑 → (0 + 𝐴) = 𝐴)

Proof of Theorem addid2d

Step	Hyp	Ref	Expression
1		muld.1	. 2 ⊢ (𝜑 → 𝐴 ∈ ℂ)
2		addid2 11088	. 2 ⊢ (𝐴 ∈ ℂ → (0 + 𝐴) = 𝐴)
3	1, 2	syl 17	1 ⊢ (𝜑 → (0 + 𝐴) = 𝐴)

Syntax hints:   → wi 4   = wceq 1539   ∈ wcel 2108  (class class class)co 7255  ℂcc 10800  0cc0 10802   + caddc 10805

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-10 2139  ax-11 2156  ax-12 2173  ax-ext 2709  ax-sep 5218  ax-nul 5225  ax-pow 5283  ax-pr 5347  ax-un 7566  ax-resscn 10859  ax-1cn 10860  ax-icn 10861  ax-addcl 10862  ax-addrcl 10863  ax-mulcl 10864  ax-mulrcl 10865  ax-mulcom 10866  ax-addass 10867  ax-mulass 10868  ax-distr 10869  ax-i2m1 10870  ax-1ne0 10871  ax-1rid 10872  ax-rnegex 10873  ax-rrecex 10874  ax-cnre 10875  ax-pre-lttri 10876  ax-pre-lttrn 10877  ax-pre-ltadd 10878

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-3or 1086  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1784  df-nf 1788  df-sb 2069  df-mo 2540  df-eu 2569  df-clab 2716  df-cleq 2730  df-clel 2817  df-nfc 2888  df-ne 2943  df-nel 3049  df-ral 3068  df-rex 3069  df-rab 3072  df-v 3424  df-sbc 3712  df-csb 3829  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-nul 4254  df-if 4457  df-pw 4532  df-sn 4559  df-pr 4561  df-op 4565  df-uni 4837  df-br 5071  df-opab 5133  df-mpt 5154  df-id 5480  df-po 5494  df-so 5495  df-xp 5586  df-rel 5587  df-cnv 5588  df-co 5589  df-dm 5590  df-rn 5591  df-res 5592  df-ima 5593  df-iota 6376  df-fun 6420  df-fn 6421  df-f 6422  df-f1 6423  df-fo 6424  df-f1o 6425  df-fv 6426  df-ov 7258  df-er 8456  df-en 8692  df-dom 8693  df-sdom 8694  df-pnf 10942  df-mnf 10943  df-ltxr 10945

This theorem is referenced by:  negeu  11141  subge0  11418  sublt0d  11531  un0addcl  12196  lincmb01cmp  13156  ico01fl0  13467  discr  13883  ccatlid  14219  swrdfv0  14290  swrdpfx  14348  pfxpfx  14349  cats1un  14362  swrdccatin2  14370  cshwidx0mod  14446  cshw1  14463  relexpaddg  14692  rennim  14878  max0add  14950  fsumsplit  15381  sumsplit  15408  isumsplit  15480  arisum2  15501  binomfallfaclem2  15678  efaddlem  15730  eftlub  15746  ef4p  15750  rpnnen2lem11  15861  moddvds  15902  divalglem9  16038  sadadd2lem2  16085  sadcaddlem  16092  gcdmultipled  16170  pcmpt  16521  4sqlem11  16584  vdwlem6  16615  gsumsgrpccat  18393  gsumccatOLD  18394  mulgnn0dir  18648  sylow1lem1  19118  efgsval2  19254  efgsp1  19258  zaddablx  19388  pgpfaclem1  19599  regsumfsum  20578  regsumsupp  20739  mplcoe5  21151  nrmmetd  23636  blcvx  23867  xrsxmet  23878  reparphti  24066  nulmbl  24604  itg2splitlem  24818  itg2split  24819  itg2monolem1  24820  itgsplitioo  24907  ditgsplit  24930  dvcnp2  24989  dvcmul  25013  dvcmulf  25014  dvmptcmul  25033  dveflem  25048  dvef  25049  dvlipcn  25063  dvlt0  25074  plymullem1  25280  coeeulem  25290  dgradd2  25334  dgrmulc  25337  plydivlem3  25360  aareccl  25391  taylthlem1  25437  sin2kpi  25545  cos2kpi  25546  coshalfpim  25557  sinkpi  25583  chordthmlem3  25889  chordthmlem5  25891  dcubic1lem  25898  dcubic  25901  atancj  25965  atanlogaddlem  25968  atanlogsublem  25970  scvxcvx  26040  zetacvg  26069  ftalem5  26131  ftalem7  26133  basellem3  26137  chtublem  26264  2sqn0  26487  2sqnn  26492  rplogsumlem2  26538  dchrisumlem1  26542  pntrlog2bndlem2  26631  brbtwn2  27176  axlowdimlem16  27228  axeuclidlem  27233  elntg2  27256  eucrct2eupth  28510  2clwwlk2clwwlk  28615  bcm1n  31018  wrdt2ind  31127  esumpfinvallem  31942  signsplypnf  32429  fsum2dsub  32487  logdivsqrle  32530  revpfxsfxrev  32977  cvxpconn  33104  cvxsconn  33105  fwddifnp1  34394  tan2h  35696  poimirlem16  35720  mbfposadd  35751  itg2addnc  35758  ftc1anclem5  35781  bfplem2  35908  aks4d1p1p4  40007  aks4d1p7d1  40018  sticksstones10  40039  sticksstones22  40052  dffltz  40387  3cubeslem3r  40425  pellexlem6  40572  jm2.18  40726  sqrtcval  41138  relexpaddss  41215  int-add02d  41685  sub2times  42702  fzisoeu  42729  xralrple2  42783  cosknegpi  43300  dvsinax  43344  dvasinbx  43351  dvnxpaek  43373  dvnmul  43374  stoweidlem1  43432  stoweidlem13  43444  stoweidlem42  43473  stirlinglem5  43509  stirlinglem11  43515  fourierdlem42  43580  fourierdlem51  43588  fourierdlem88  43625  fourierdlem103  43640  fourierdlem104  43641  fourierdlem107  43644  sqwvfoura  43659  sqwvfourb  43660  fouriersw  43662  elaa2lem  43664  hspmbllem1  44054  cnambpcma  44674  readdcnnred  44683  nn0mnd  45261  altgsumbcALT  45577  nn0sumshdiglemA  45853  line2xlem  45987  line2x  45988  itschlc0yqe  45994  itsclc0yqsollem1  45996  itschlc0xyqsol1  46000  itschlc0xyqsol  46001  2itscp  46015