Theorem addlidd 11338

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 11320	. 2 ⊢ (𝐴 ∈ ℂ → (0 + 𝐴) = 𝐴)
3	1, 2	syl 17	1 ⊢ (𝜑 → (0 + 𝐴) = 𝐴)

Syntax hints:   → wi 4   = wceq 1542   ∈ wcel 2114  (class class class)co 7360  ℂcc 11027  0cc0 11029   + caddc 11032

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 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2709  ax-sep 5231  ax-nul 5241  ax-pow 5302  ax-pr 5370  ax-un 7682  ax-resscn 11086  ax-1cn 11087  ax-icn 11088  ax-addcl 11089  ax-addrcl 11090  ax-mulcl 11091  ax-mulrcl 11092  ax-mulcom 11093  ax-addass 11094  ax-mulass 11095  ax-distr 11096  ax-i2m1 11097  ax-1ne0 11098  ax-1rid 11099  ax-rnegex 11100  ax-rrecex 11101  ax-cnre 11102  ax-pre-lttri 11103  ax-pre-lttrn 11104  ax-pre-ltadd 11105

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2540  df-eu 2570  df-clab 2716  df-cleq 2729  df-clel 2812  df-nfc 2886  df-ne 2934  df-nel 3038  df-ral 3053  df-rex 3063  df-rab 3391  df-v 3432  df-sbc 3730  df-csb 3839  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-nul 4275  df-if 4468  df-pw 4544  df-sn 4569  df-pr 4571  df-op 4575  df-uni 4852  df-br 5087  df-opab 5149  df-mpt 5168  df-id 5519  df-po 5532  df-so 5533  df-xp 5630  df-rel 5631  df-cnv 5632  df-co 5633  df-dm 5634  df-rn 5635  df-res 5636  df-ima 5637  df-iota 6448  df-fun 6494  df-fn 6495  df-f 6496  df-f1 6497  df-fo 6498  df-f1o 6499  df-fv 6500  df-ov 7363  df-er 8636  df-en 8887  df-dom 8888  df-sdom 8889  df-pnf 11172  df-mnf 11173  df-ltxr 11175

This theorem is referenced by:  negeu  11374  subge0  11654  sublt0d  11767  un0addcl  12461  lincmb01cmp  13439  ico01fl0  13769  muladdmod  13865  discr  14193  ccatlid  14540  swrdfv0  14603  swrdpfx  14660  pfxpfx  14661  cats1un  14674  swrdccatin2  14682  cshwidx0mod  14758  cshw1  14775  relexpaddg  15006  rennim  15192  max0add  15263  fsumsplit  15694  sumsplit  15721  isumsplit  15796  arisum2  15817  binomfallfaclem2  15996  efaddlem  16049  eftlub  16067  ef4p  16071  rpnnen2lem11  16182  moddvds  16223  divalglem9  16361  sadadd2lem2  16410  sadcaddlem  16417  gcdmultipled  16494  pcmpt  16854  4sqlem11  16917  vdwlem6  16948  gsumsgrpccat  18799  mulgnn0dir  19071  sylow1lem1  19564  efgsval2  19699  efgsp1  19703  zaddablx  19838  pgpfaclem1  20049  regsumfsum  21425  regsumsupp  21612  mplcoe5  22028  nrmmetd  24549  blcvx  24773  xrsxmet  24785  reparphti  24974  nulmbl  25512  itg2splitlem  25725  itg2split  25726  itg2monolem1  25727  itgsplitioo  25815  ditgsplit  25838  dvcnp2  25897  dvcmul  25921  dvcmulf  25922  dvmptcmul  25941  dveflem  25956  dvef  25957  dvlipcn  25971  dvlt0  25982  plymullem1  26189  coeeulem  26199  dgradd2  26243  dgrmulc  26246  plydivlem3  26272  aareccl  26303  taylthlem1  26350  sin2kpi  26460  cos2kpi  26461  coshalfpim  26472  sinkpi  26499  chordthmlem3  26811  chordthmlem5  26813  dcubic1lem  26820  dcubic  26823  atancj  26887  atanlogaddlem  26890  atanlogsublem  26892  scvxcvx  26963  zetacvg  26992  ftalem5  27054  ftalem7  27056  basellem3  27060  chtublem  27188  2sqn0  27411  2sqnn  27416  rplogsumlem2  27462  dchrisumlem1  27466  pntrlog2bndlem2  27555  brbtwn2  28988  axlowdimlem16  29040  axeuclidlem  29045  elntg2  29068  eucrct2eupth  30330  2clwwlk2clwwlk  30435  re0cj  32831  bcm1n  32883  wrdt2ind  33028  nn0constr  33921  constraddcl  33922  constrnegcl  33923  constrdircl  33925  constrremulcl  33927  constrrecl  33929  constrimcl  33930  constrmulcl  33931  constrreinvcl  33932  constrinvcl  33933  constrresqrtcl  33937  constrabscl  33938  2sqr3minply  33940  cos9thpiminplylem1  33942  cos9thpiminply  33948  cos9thpinconstrlem1  33949  esumpfinvallem  34234  signsplypnf  34710  fsum2dsub  34767  logdivsqrle  34810  revpfxsfxrev  35314  cvxpconn  35440  cvxsconn  35441  fwddifnp1  36363  tan2h  37947  poimirlem16  37971  mbfposadd  38002  itg2addnc  38009  ftc1anclem5  38032  bfplem2  38158  aks4d1p1p4  42524  aks4d1p7d1  42535  primrootspoweq0  42559  aks6d1c1  42569  aks6d1c5lem1  42589  sticksstones10  42608  sticksstones22  42621  bcle2d  42632  dffltz  43081  3cubeslem3r  43133  pellexlem6  43280  jm2.18  43434  sqrtcval  44086  relexpaddss  44163  int-add02d  44630  sub2times  45724  fzisoeu  45751  xralrple2  45802  cosknegpi  46315  dvsinax  46359  dvasinbx  46366  dvnxpaek  46388  dvnmul  46389  stoweidlem1  46447  stoweidlem13  46459  stoweidlem42  46488  stirlinglem5  46524  stirlinglem11  46530  fourierdlem42  46595  fourierdlem51  46603  fourierdlem88  46640  fourierdlem103  46655  fourierdlem104  46656  fourierdlem107  46659  sqwvfoura  46674  sqwvfourb  46675  fouriersw  46677  elaa2lem  46679  hspmbllem1  47072  cnambpcma  47754  readdcnnred  47763  gpg3kgrtriex  48577  nn0mnd  48667  altgsumbcALT  48841  nn0sumshdiglemA  49107  line2xlem  49241  line2x  49242  itschlc0yqe  49248  itsclc0yqsollem1  49250  itschlc0xyqsol1  49254  itschlc0xyqsol  49255  2itscp  49269