Theorem addlidd 11335

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

Hypothesis

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

Assertion

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

Proof of Theorem addlidd

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

Syntax hints:   → wi 4   = wceq 1540   ∈ wcel 2109  (class class class)co 7353  ℂcc 11026  0cc0 11028   + caddc 11031

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2701  ax-sep 5238  ax-nul 5248  ax-pow 5307  ax-pr 5374  ax-un 7675  ax-resscn 11085  ax-1cn 11086  ax-icn 11087  ax-addcl 11088  ax-addrcl 11089  ax-mulcl 11090  ax-mulrcl 11091  ax-mulcom 11092  ax-addass 11093  ax-mulass 11094  ax-distr 11095  ax-i2m1 11096  ax-1ne0 11097  ax-1rid 11098  ax-rnegex 11099  ax-rrecex 11100  ax-cnre 11101  ax-pre-lttri 11102  ax-pre-lttrn 11103  ax-pre-ltadd 11104

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2533  df-eu 2562  df-clab 2708  df-cleq 2721  df-clel 2803  df-nfc 2878  df-ne 2926  df-nel 3030  df-ral 3045  df-rex 3054  df-rab 3397  df-v 3440  df-sbc 3745  df-csb 3854  df-dif 3908  df-un 3910  df-in 3912  df-ss 3922  df-nul 4287  df-if 4479  df-pw 4555  df-sn 4580  df-pr 4582  df-op 4586  df-uni 4862  df-br 5096  df-opab 5158  df-mpt 5177  df-id 5518  df-po 5531  df-so 5532  df-xp 5629  df-rel 5630  df-cnv 5631  df-co 5632  df-dm 5633  df-rn 5634  df-res 5635  df-ima 5636  df-iota 6442  df-fun 6488  df-fn 6489  df-f 6490  df-f1 6491  df-fo 6492  df-f1o 6493  df-fv 6494  df-ov 7356  df-er 8632  df-en 8880  df-dom 8881  df-sdom 8882  df-pnf 11170  df-mnf 11171  df-ltxr 11173

This theorem is referenced by:  negeu  11371  subge0  11651  sublt0d  11764  un0addcl  12435  lincmb01cmp  13416  ico01fl0  13741  muladdmod  13837  discr  14165  ccatlid  14511  swrdfv0  14574  swrdpfx  14631  pfxpfx  14632  cats1un  14645  swrdccatin2  14653  cshwidx0mod  14729  cshw1  14746  relexpaddg  14978  rennim  15164  max0add  15235  fsumsplit  15666  sumsplit  15693  isumsplit  15765  arisum2  15786  binomfallfaclem2  15965  efaddlem  16018  eftlub  16036  ef4p  16040  rpnnen2lem11  16151  moddvds  16192  divalglem9  16330  sadadd2lem2  16379  sadcaddlem  16386  gcdmultipled  16463  pcmpt  16822  4sqlem11  16885  vdwlem6  16916  gsumsgrpccat  18732  mulgnn0dir  19001  sylow1lem1  19495  efgsval2  19630  efgsp1  19634  zaddablx  19769  pgpfaclem1  19980  regsumfsum  21360  regsumsupp  21547  mplcoe5  21963  nrmmetd  24478  blcvx  24702  xrsxmet  24714  reparphti  24912  reparphtiOLD  24913  nulmbl  25452  itg2splitlem  25665  itg2split  25666  itg2monolem1  25667  itgsplitioo  25755  ditgsplit  25778  dvcnp2  25837  dvcnp2OLD  25838  dvcmul  25863  dvcmulf  25864  dvmptcmul  25884  dveflem  25899  dvef  25900  dvlipcn  25915  dvlt0  25926  plymullem1  26135  coeeulem  26145  dgradd2  26190  dgrmulc  26193  plydivlem3  26219  aareccl  26250  taylthlem1  26297  sin2kpi  26408  cos2kpi  26409  coshalfpim  26420  sinkpi  26447  chordthmlem3  26760  chordthmlem5  26762  dcubic1lem  26769  dcubic  26772  atancj  26836  atanlogaddlem  26839  atanlogsublem  26841  scvxcvx  26912  zetacvg  26941  ftalem5  27003  ftalem7  27005  basellem3  27009  chtublem  27138  2sqn0  27361  2sqnn  27366  rplogsumlem2  27412  dchrisumlem1  27416  pntrlog2bndlem2  27505  brbtwn2  28868  axlowdimlem16  28920  axeuclidlem  28925  elntg2  28948  eucrct2eupth  30207  2clwwlk2clwwlk  30312  re0cj  32700  bcm1n  32751  wrdt2ind  32908  nn0constr  33727  constraddcl  33728  constrnegcl  33729  constrdircl  33731  constrremulcl  33733  constrrecl  33735  constrimcl  33736  constrmulcl  33737  constrreinvcl  33738  constrinvcl  33739  constrresqrtcl  33743  constrabscl  33744  2sqr3minply  33746  cos9thpiminplylem1  33748  cos9thpiminply  33754  cos9thpinconstrlem1  33755  esumpfinvallem  34040  signsplypnf  34517  fsum2dsub  34574  logdivsqrle  34617  revpfxsfxrev  35088  cvxpconn  35214  cvxsconn  35215  fwddifnp1  36138  tan2h  37591  poimirlem16  37615  mbfposadd  37646  itg2addnc  37653  ftc1anclem5  37676  bfplem2  37802  aks4d1p1p4  42044  aks4d1p7d1  42055  primrootspoweq0  42079  aks6d1c1  42089  aks6d1c5lem1  42109  sticksstones10  42128  sticksstones22  42141  bcle2d  42152  dffltz  42607  3cubeslem3r  42660  pellexlem6  42807  jm2.18  42961  sqrtcval  43614  relexpaddss  43691  int-add02d  44158  sub2times  45255  fzisoeu  45282  xralrple2  45334  cosknegpi  45851  dvsinax  45895  dvasinbx  45902  dvnxpaek  45924  dvnmul  45925  stoweidlem1  45983  stoweidlem13  45995  stoweidlem42  46024  stirlinglem5  46060  stirlinglem11  46066  fourierdlem42  46131  fourierdlem51  46139  fourierdlem88  46176  fourierdlem103  46191  fourierdlem104  46192  fourierdlem107  46195  sqwvfoura  46210  sqwvfourb  46211  fouriersw  46213  elaa2lem  46215  hspmbllem1  46608  cnambpcma  47279  readdcnnred  47288  gpg3kgrtriex  48064  nn0mnd  48151  altgsumbcALT  48325  nn0sumshdiglemA  48592  line2xlem  48726  line2x  48727  itschlc0yqe  48733  itsclc0yqsollem1  48735  itschlc0xyqsol1  48739  itschlc0xyqsol  48740  2itscp  48754