Theorem addlidd 11445

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

Syntax hints:   → wi 4   = wceq 1534   ∈ wcel 2099  (class class class)co 7420  ℂcc 11136  0cc0 11138   + caddc 11141

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-10 2130  ax-11 2147  ax-12 2167  ax-ext 2699  ax-sep 5299  ax-nul 5306  ax-pow 5365  ax-pr 5429  ax-un 7740  ax-resscn 11195  ax-1cn 11196  ax-icn 11197  ax-addcl 11198  ax-addrcl 11199  ax-mulcl 11200  ax-mulrcl 11201  ax-mulcom 11202  ax-addass 11203  ax-mulass 11204  ax-distr 11205  ax-i2m1 11206  ax-1ne0 11207  ax-1rid 11208  ax-rnegex 11209  ax-rrecex 11210  ax-cnre 11211  ax-pre-lttri 11212  ax-pre-lttrn 11213  ax-pre-ltadd 11214

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 847  df-3or 1086  df-3an 1087  df-tru 1537  df-fal 1547  df-ex 1775  df-nf 1779  df-sb 2061  df-mo 2530  df-eu 2559  df-clab 2706  df-cleq 2720  df-clel 2806  df-nfc 2881  df-ne 2938  df-nel 3044  df-ral 3059  df-rex 3068  df-rab 3430  df-v 3473  df-sbc 3777  df-csb 3893  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-nul 4324  df-if 4530  df-pw 4605  df-sn 4630  df-pr 4632  df-op 4636  df-uni 4909  df-br 5149  df-opab 5211  df-mpt 5232  df-id 5576  df-po 5590  df-so 5591  df-xp 5684  df-rel 5685  df-cnv 5686  df-co 5687  df-dm 5688  df-rn 5689  df-res 5690  df-ima 5691  df-iota 6500  df-fun 6550  df-fn 6551  df-f 6552  df-f1 6553  df-fo 6554  df-f1o 6555  df-fv 6556  df-ov 7423  df-er 8724  df-en 8964  df-dom 8965  df-sdom 8966  df-pnf 11280  df-mnf 11281  df-ltxr 11283

This theorem is referenced by:  negeu  11480  subge0  11757  sublt0d  11870  un0addcl  12535  lincmb01cmp  13504  ico01fl0  13816  discr  14234  ccatlid  14568  swrdfv0  14631  swrdpfx  14689  pfxpfx  14690  cats1un  14703  swrdccatin2  14711  cshwidx0mod  14787  cshw1  14804  relexpaddg  15032  rennim  15218  max0add  15289  fsumsplit  15719  sumsplit  15746  isumsplit  15818  arisum2  15839  binomfallfaclem2  16016  efaddlem  16069  eftlub  16085  ef4p  16089  rpnnen2lem11  16200  moddvds  16241  divalglem9  16377  sadadd2lem2  16424  sadcaddlem  16431  gcdmultipled  16509  pcmpt  16860  4sqlem11  16923  vdwlem6  16954  gsumsgrpccat  18791  mulgnn0dir  19058  sylow1lem1  19552  efgsval2  19687  efgsp1  19691  zaddablx  19826  pgpfaclem1  20037  regsumfsum  21367  regsumsupp  21553  mplcoe5  21977  nrmmetd  24482  blcvx  24713  xrsxmet  24724  reparphti  24922  reparphtiOLD  24923  nulmbl  25463  itg2splitlem  25677  itg2split  25678  itg2monolem1  25679  itgsplitioo  25766  ditgsplit  25789  dvcnp2  25848  dvcnp2OLD  25849  dvcmul  25874  dvcmulf  25875  dvmptcmul  25895  dveflem  25910  dvef  25911  dvlipcn  25926  dvlt0  25937  plymullem1  26147  coeeulem  26157  dgradd2  26202  dgrmulc  26205  plydivlem3  26229  aareccl  26260  taylthlem1  26307  sin2kpi  26417  cos2kpi  26418  coshalfpim  26429  sinkpi  26455  chordthmlem3  26765  chordthmlem5  26767  dcubic1lem  26774  dcubic  26777  atancj  26841  atanlogaddlem  26844  atanlogsublem  26846  scvxcvx  26917  zetacvg  26946  ftalem5  27008  ftalem7  27010  basellem3  27014  chtublem  27143  2sqn0  27366  2sqnn  27371  rplogsumlem2  27417  dchrisumlem1  27421  pntrlog2bndlem2  27510  brbtwn2  28715  axlowdimlem16  28767  axeuclidlem  28772  elntg2  28795  eucrct2eupth  30054  2clwwlk2clwwlk  30159  bcm1n  32563  wrdt2ind  32674  esumpfinvallem  33693  signsplypnf  34182  fsum2dsub  34239  logdivsqrle  34282  revpfxsfxrev  34725  cvxpconn  34852  cvxsconn  34853  fwddifnp1  35761  tan2h  37085  poimirlem16  37109  mbfposadd  37140  itg2addnc  37147  ftc1anclem5  37170  bfplem2  37296  aks4d1p1p4  41542  aks4d1p7d1  41553  primrootspoweq0  41577  aks6d1c1  41587  aks6d1c5lem1  41607  sticksstones10  41627  sticksstones22  41640  bcle2d  41651  dffltz  42058  3cubeslem3r  42107  pellexlem6  42254  jm2.18  42409  sqrtcval  43071  relexpaddss  43148  int-add02d  43615  sub2times  44654  fzisoeu  44682  xralrple2  44736  cosknegpi  45257  dvsinax  45301  dvasinbx  45308  dvnxpaek  45330  dvnmul  45331  stoweidlem1  45389  stoweidlem13  45401  stoweidlem42  45430  stirlinglem5  45466  stirlinglem11  45472  fourierdlem42  45537  fourierdlem51  45545  fourierdlem88  45582  fourierdlem103  45597  fourierdlem104  45598  fourierdlem107  45601  sqwvfoura  45616  sqwvfourb  45617  fouriersw  45619  elaa2lem  45621  hspmbllem1  46014  cnambpcma  46674  readdcnnred  46683  nn0mnd  47241  altgsumbcALT  47417  nn0sumshdiglemA  47692  line2xlem  47826  line2x  47827  itschlc0yqe  47833  itsclc0yqsollem1  47835  itschlc0xyqsol1  47839  itschlc0xyqsol  47840  2itscp  47854