Theorem addlidd 11410

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

Syntax hints:   → wi 4   = wceq 1568   ∈ wcel 2141  (class class class)co 7410  ℂcc 11097  0cc0 11099   + caddc 11102

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1823  ax-4 1837  ax-5 1938  ax-6 1995  ax-7 2036  ax-8 2143  ax-9 2151  ax-10 2174  ax-11 2190  ax-12 2211  ax-ext 2733  ax-sep 5256  ax-nul 5268  ax-pow 5336  ax-pr 5404  ax-un 7732  ax-resscn 11156  ax-1cn 11157  ax-icn 11158  ax-addcl 11159  ax-addrcl 11160  ax-mulcl 11161  ax-mulrcl 11162  ax-mulcom 11163  ax-addass 11164  ax-mulass 11165  ax-distr 11166  ax-i2m1 11167  ax-1ne0 11168  ax-1rid 11169  ax-rnegex 11170  ax-rrecex 11171  ax-cnre 11172  ax-pre-lttri 11173  ax-pre-lttrn 11174  ax-pre-ltadd 11175

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3or 1102  df-3an 1103  df-tru 1571  df-fal 1581  df-ex 1808  df-nf 1812  df-sb 2095  df-mo 2565  df-eu 2595  df-clab 2740  df-cleq 2753  df-clel 2836  df-nfc 2910  df-ne 2957  df-nel 3063  df-ral 3078  df-rex 3088  df-rab 3415  df-v 3455  df-sbc 3744  df-csb 3853  df-dif 3907  df-un 3909  df-in 3911  df-ss 3921  df-nul 4286  df-if 4487  df-pw 4563  df-sn 4589  df-pr 4591  df-op 4595  df-uni 4872  df-br 5109  df-opab 5173  df-mpt 5192  df-id 5556  df-po 5569  df-so 5570  df-xp 5667  df-rel 5668  df-cnv 5669  df-co 5670  df-dm 5671  df-rn 5672  df-res 5673  df-ima 5674  df-iota 6492  df-fun 6538  df-fn 6539  df-f 6540  df-f1 6541  df-fo 6542  df-f1o 6543  df-fv 6544  df-ov 7413  df-er 8693  df-en 8943  df-dom 8944  df-sdom 8945  df-pnf 11244  df-mnf 11245  df-ltxr 11247

This theorem is referenced by:  negeu  11446  subge0  11726  sublt0d  11839  un0addcl  12536  lincmb01cmp  13521  ico01fl0  13851  muladdmod  13947  discr  14275  ccatlid  14623  swrdfv0  14686  swrdpfx  14743  pfxpfx  14744  cats1un  14757  swrdccatin2  14765  cshwidx0mod  14841  cshw1  14858  relexpaddg  15089  rennim  15289  max0add  15360  fsumsplit  15791  sumsplit  15818  isumsplit  15893  arisum2  15914  binomfallfaclem2  16093  efaddlem  16146  eftlub  16164  ef4p  16168  rpnnen2lem11  16279  moddvds  16320  divalglem9  16458  sadadd2lem2  16507  sadcaddlem  16514  gcdmultipled  16591  pcmpt  16951  4sqlem11  17014  vdwlem6  17045  gsumsgrpccat  18898  mulgnn0dir  19169  sylow1lem1  19667  efgsval2  19802  efgsp1  19806  zaddablx  19941  pgpfaclem1  20152  regsumfsum  21564  regsumsupp  21751  mplcoe5  22170  nrmmetd  24710  blcvx  24934  xrsxmet  24946  reparphti  25135  nulmbl  25673  itg2splitlem  25886  itg2split  25887  itg2monolem1  25888  itgsplitioo  25976  ditgsplit  25999  dvcnp2  26058  dvcmul  26082  dvcmulf  26083  dvmptcmul  26102  dveflem  26117  dvef  26118  dvlipcn  26132  dvlt0  26143  plymullem1  26350  coeeulem  26360  dgradd2  26404  dgrmulc  26407  plydivlem3  26435  aareccl  26466  taylthlem1  26512  sin2kpi  26624  cos2kpi  26625  coshalfpim  26636  sinkpi  26663  chordthmlem3  26975  chordthmlem5  26977  dcubic1lem  26984  dcubic  26987  atancj  27051  atanlogaddlem  27054  atanlogsublem  27056  scvxcvx  27126  zetacvg  27155  ftalem5  27217  ftalem7  27219  basellem3  27223  chtublem  27351  2sqn0  27574  2sqnn  27579  rplogsumlem2  27625  dchrisumlem1  27629  pntrlog2bndlem2  27718  brbtwn2  29221  axlowdimlem16  29273  axeuclidlem  29278  elntg2  29301  eucrct2eupth  30562  2clwwlk2clwwlk  30667  re0cj  33054  bcm1n  33106  wrdt2ind  33239  nn0constr  34117  constraddcl  34118  constrnegcl  34119  constrdircl  34121  constrremulcl  34123  constrrecl  34125  constrimcl  34126  constrmulcl  34127  constrreinvcl  34128  constrinvcl  34129  constrresqrtcl  34133  constrabscl  34134  2sqr3minply  34136  cos9thpiminplylem1  34138  cos9thpiminply  34144  cos9thpinconstrlem1  34145  esumpfinvallem  34430  signsplypnf  34903  fsum2dsub  34960  logdivsqrle  35003  revpfxsfxrev  35561  cvxpconn  35688  cvxsconn  35689  fwddifnp1  36611  tan2h  38207  poimirlem16  38231  mbfposadd  38262  itg2addnc  38269  ftc1anclem5  38292  bfplem2  38418  aks4d1p1p4  42784  aks4d1p7d1  42795  primrootspoweq0  42819  aks6d1c1  42829  aks6d1c5lem1  42849  sticksstones10  42868  sticksstones22  42881  bcle2d  42892  dffltz  43314  3cubeslem3r  43366  pellexlem6  43509  jm2.18  43663  sqrtcval  44315  relexpaddss  44392  int-add02d  44859  sub2times  45940  fzisoeu  45967  xralrple2  46018  cosknegpi  46531  dvsinax  46575  dvasinbx  46582  dvnxpaek  46604  dvnmul  46605  stoweidlem1  46663  stoweidlem13  46675  stoweidlem42  46704  stirlinglem5  46740  stirlinglem11  46746  fourierdlem42  46811  fourierdlem51  46819  fourierdlem88  46856  fourierdlem103  46871  fourierdlem104  46872  fourierdlem107  46875  sqwvfoura  46890  sqwvfourb  46891  fouriersw  46893  elaa2lem  46895  hspmbllem1  47288  cnambpcma  47976  readdcnnred  47985  gpg3kgrtriex  48799  nn0mnd  48889  altgsumbcALT  49078  nn0sumshdiglemA  49344  line2xlem  49478  line2x  49479  itschlc0yqe  49485  itsclc0yqsollem1  49487  itschlc0xyqsol1  49491  itschlc0xyqsol  49492  2itscp  49506