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 11028  0cc0 11030   + caddc 11033

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 5242  ax-nul 5252  ax-pow 5311  ax-pr 5378  ax-un 7682  ax-resscn 11087  ax-1cn 11088  ax-icn 11089  ax-addcl 11090  ax-addrcl 11091  ax-mulcl 11092  ax-mulrcl 11093  ax-mulcom 11094  ax-addass 11095  ax-mulass 11096  ax-distr 11097  ax-i2m1 11098  ax-1ne0 11099  ax-1rid 11100  ax-rnegex 11101  ax-rrecex 11102  ax-cnre 11103  ax-pre-lttri 11104  ax-pre-lttrn 11105  ax-pre-ltadd 11106

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 3062  df-rab 3401  df-v 3443  df-sbc 3742  df-csb 3851  df-dif 3905  df-un 3907  df-in 3909  df-ss 3919  df-nul 4287  df-if 4481  df-pw 4557  df-sn 4582  df-pr 4584  df-op 4588  df-uni 4865  df-br 5100  df-opab 5162  df-mpt 5181  df-id 5520  df-po 5533  df-so 5534  df-xp 5631  df-rel 5632  df-cnv 5633  df-co 5634  df-dm 5635  df-rn 5636  df-res 5637  df-ima 5638  df-iota 6449  df-fun 6495  df-fn 6496  df-f 6497  df-f1 6498  df-fo 6499  df-f1o 6500  df-fv 6501  df-ov 7363  df-er 8637  df-en 8888  df-dom 8889  df-sdom 8890  df-pnf 11172  df-mnf 11173  df-ltxr 11175

This theorem is referenced by:  negeu  11374  subge0  11654  sublt0d  11767  un0addcl  12438  lincmb01cmp  13415  ico01fl0  13743  muladdmod  13839  discr  14167  ccatlid  14514  swrdfv0  14577  swrdpfx  14634  pfxpfx  14635  cats1un  14648  swrdccatin2  14656  cshwidx0mod  14732  cshw1  14749  relexpaddg  14980  rennim  15166  max0add  15237  fsumsplit  15668  sumsplit  15695  isumsplit  15767  arisum2  15788  binomfallfaclem2  15967  efaddlem  16020  eftlub  16038  ef4p  16042  rpnnen2lem11  16153  moddvds  16194  divalglem9  16332  sadadd2lem2  16381  sadcaddlem  16388  gcdmultipled  16465  pcmpt  16824  4sqlem11  16887  vdwlem6  16918  gsumsgrpccat  18769  mulgnn0dir  19038  sylow1lem1  19531  efgsval2  19666  efgsp1  19670  zaddablx  19805  pgpfaclem1  20016  regsumfsum  21394  regsumsupp  21581  mplcoe5  21999  nrmmetd  24522  blcvx  24746  xrsxmet  24758  reparphti  24956  reparphtiOLD  24957  nulmbl  25496  itg2splitlem  25709  itg2split  25710  itg2monolem1  25711  itgsplitioo  25799  ditgsplit  25822  dvcnp2  25881  dvcnp2OLD  25882  dvcmul  25907  dvcmulf  25908  dvmptcmul  25928  dveflem  25943  dvef  25944  dvlipcn  25959  dvlt0  25970  plymullem1  26179  coeeulem  26189  dgradd2  26234  dgrmulc  26237  plydivlem3  26263  aareccl  26294  taylthlem1  26341  sin2kpi  26452  cos2kpi  26453  coshalfpim  26464  sinkpi  26491  chordthmlem3  26804  chordthmlem5  26806  dcubic1lem  26813  dcubic  26816  atancj  26880  atanlogaddlem  26883  atanlogsublem  26885  scvxcvx  26956  zetacvg  26985  ftalem5  27047  ftalem7  27049  basellem3  27053  chtublem  27182  2sqn0  27405  2sqnn  27410  rplogsumlem2  27456  dchrisumlem1  27460  pntrlog2bndlem2  27549  brbtwn2  28961  axlowdimlem16  29013  axeuclidlem  29018  elntg2  29041  eucrct2eupth  30303  2clwwlk2clwwlk  30408  re0cj  32804  bcm1n  32856  wrdt2ind  33016  nn0constr  33899  constraddcl  33900  constrnegcl  33901  constrdircl  33903  constrremulcl  33905  constrrecl  33907  constrimcl  33908  constrmulcl  33909  constrreinvcl  33910  constrinvcl  33911  constrresqrtcl  33915  constrabscl  33916  2sqr3minply  33918  cos9thpiminplylem1  33920  cos9thpiminply  33926  cos9thpinconstrlem1  33927  esumpfinvallem  34212  signsplypnf  34688  fsum2dsub  34745  logdivsqrle  34788  revpfxsfxrev  35291  cvxpconn  35417  cvxsconn  35418  fwddifnp1  36340  tan2h  37784  poimirlem16  37808  mbfposadd  37839  itg2addnc  37846  ftc1anclem5  37869  bfplem2  37995  aks4d1p1p4  42362  aks4d1p7d1  42373  primrootspoweq0  42397  aks6d1c1  42407  aks6d1c5lem1  42427  sticksstones10  42446  sticksstones22  42459  bcle2d  42470  dffltz  42913  3cubeslem3r  42965  pellexlem6  43112  jm2.18  43266  sqrtcval  43918  relexpaddss  43995  int-add02d  44462  sub2times  45557  fzisoeu  45584  xralrple2  45635  cosknegpi  46149  dvsinax  46193  dvasinbx  46200  dvnxpaek  46222  dvnmul  46223  stoweidlem1  46281  stoweidlem13  46293  stoweidlem42  46322  stirlinglem5  46358  stirlinglem11  46364  fourierdlem42  46429  fourierdlem51  46437  fourierdlem88  46474  fourierdlem103  46489  fourierdlem104  46490  fourierdlem107  46493  sqwvfoura  46508  sqwvfourb  46509  fouriersw  46511  elaa2lem  46513  hspmbllem1  46906  cnambpcma  47576  readdcnnred  47585  gpg3kgrtriex  48371  nn0mnd  48461  altgsumbcALT  48635  nn0sumshdiglemA  48901  line2xlem  49035  line2x  49036  itschlc0yqe  49042  itsclc0yqsollem1  49044  itschlc0xyqsol1  49048  itschlc0xyqsol  49049  2itscp  49063