Theorem addlidd 11395

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

Syntax hints:   → wi 4   = wceq 1561   ∈ wcel 2143  (class class class)co 7396  ℂcc 11082  0cc0 11084   + caddc 11087

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1816  ax-4 1830  ax-5 1931  ax-6 1988  ax-7 2029  ax-8 2145  ax-9 2153  ax-10 2176  ax-11 2192  ax-12 2213  ax-ext 2735  ax-sep 5247  ax-nul 5257  ax-pow 5323  ax-pr 5391  ax-un 7718  ax-resscn 11141  ax-1cn 11142  ax-icn 11143  ax-addcl 11144  ax-addrcl 11145  ax-mulcl 11146  ax-mulrcl 11147  ax-mulcom 11148  ax-addass 11149  ax-mulass 11150  ax-distr 11151  ax-i2m1 11152  ax-1ne0 11153  ax-1rid 11154  ax-rnegex 11155  ax-rrecex 11156  ax-cnre 11157  ax-pre-lttri 11158  ax-pre-lttrn 11159  ax-pre-ltadd 11160

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-3or 1100  df-3an 1101  df-tru 1564  df-fal 1574  df-ex 1801  df-nf 1805  df-sb 2092  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2838  df-nfc 2912  df-ne 2959  df-nel 3063  df-ral 3078  df-rex 3088  df-rab 3416  df-v 3457  df-sbc 3746  df-csb 3854  df-dif 3908  df-un 3910  df-in 3912  df-ss 3922  df-nul 4287  df-if 4482  df-pw 4558  df-sn 4584  df-pr 4586  df-op 4590  df-uni 4867  df-br 5102  df-opab 5164  df-mpt 5183  df-id 5543  df-po 5556  df-so 5557  df-xp 5654  df-rel 5655  df-cnv 5656  df-co 5657  df-dm 5658  df-rn 5659  df-res 5660  df-ima 5661  df-iota 6477  df-fun 6523  df-fn 6524  df-f 6525  df-f1 6526  df-fo 6527  df-f1o 6528  df-fv 6529  df-ov 7399  df-er 8678  df-en 8928  df-dom 8929  df-sdom 8930  df-pnf 11229  df-mnf 11230  df-ltxr 11232

This theorem is referenced by:  negeu  11431  subge0  11711  sublt0d  11824  un0addcl  12524  lincmb01cmp  13509  ico01fl0  13839  muladdmod  13935  discr  14263  ccatlid  14610  swrdfv0  14673  swrdpfx  14730  pfxpfx  14731  cats1un  14744  swrdccatin2  14752  cshwidx0mod  14828  cshw1  14845  relexpaddg  15076  rennim  15276  max0add  15347  fsumsplit  15778  sumsplit  15805  isumsplit  15880  arisum2  15901  binomfallfaclem2  16080  efaddlem  16133  eftlub  16151  ef4p  16155  rpnnen2lem11  16266  moddvds  16307  divalglem9  16445  sadadd2lem2  16494  sadcaddlem  16501  gcdmultipled  16578  pcmpt  16938  4sqlem11  17001  vdwlem6  17032  gsumsgrpccat  18884  mulgnn0dir  19156  sylow1lem1  19648  efgsval2  19783  efgsp1  19787  zaddablx  19922  pgpfaclem1  20133  regsumfsum  21494  regsumsupp  21681  mplcoe5  22100  nrmmetd  24641  blcvx  24865  xrsxmet  24877  reparphti  25066  nulmbl  25604  itg2splitlem  25817  itg2split  25818  itg2monolem1  25819  itgsplitioo  25907  ditgsplit  25930  dvcnp2  25989  dvcmul  26013  dvcmulf  26014  dvmptcmul  26033  dveflem  26048  dvef  26049  dvlipcn  26063  dvlt0  26074  plymullem1  26281  coeeulem  26291  dgradd2  26335  dgrmulc  26338  plydivlem3  26366  aareccl  26397  taylthlem1  26443  sin2kpi  26555  cos2kpi  26556  coshalfpim  26567  sinkpi  26594  chordthmlem3  26906  chordthmlem5  26908  dcubic1lem  26915  dcubic  26918  atancj  26982  atanlogaddlem  26985  atanlogsublem  26987  scvxcvx  27057  zetacvg  27086  ftalem5  27148  ftalem7  27150  basellem3  27154  chtublem  27282  2sqn0  27505  2sqnn  27510  rplogsumlem2  27556  dchrisumlem1  27560  pntrlog2bndlem2  27649  brbtwn2  29113  axlowdimlem16  29165  axeuclidlem  29170  elntg2  29193  eucrct2eupth  30454  2clwwlk2clwwlk  30559  re0cj  32951  bcm1n  33003  wrdt2ind  33137  nn0constr  34060  constraddcl  34061  constrnegcl  34062  constrdircl  34064  constrremulcl  34066  constrrecl  34068  constrimcl  34069  constrmulcl  34070  constrreinvcl  34071  constrinvcl  34072  constrresqrtcl  34076  constrabscl  34077  2sqr3minply  34079  cos9thpiminplylem1  34081  cos9thpiminply  34087  cos9thpinconstrlem1  34088  esumpfinvallem  34373  signsplypnf  34846  fsum2dsub  34903  logdivsqrle  34946  revpfxsfxrev  35470  cvxpconn  35597  cvxsconn  35598  fwddifnp1  36520  tan2h  38116  poimirlem16  38140  mbfposadd  38171  itg2addnc  38178  ftc1anclem5  38201  bfplem2  38327  aks4d1p1p4  42693  aks4d1p7d1  42704  primrootspoweq0  42728  aks6d1c1  42738  aks6d1c5lem1  42758  sticksstones10  42777  sticksstones22  42790  bcle2d  42801  dffltz  43221  3cubeslem3r  43273  pellexlem6  43416  jm2.18  43570  sqrtcval  44222  relexpaddss  44299  int-add02d  44766  sub2times  45843  fzisoeu  45870  xralrple2  45921  cosknegpi  46434  dvsinax  46478  dvasinbx  46485  dvnxpaek  46507  dvnmul  46508  stoweidlem1  46566  stoweidlem13  46578  stoweidlem42  46607  stirlinglem5  46643  stirlinglem11  46649  fourierdlem42  46714  fourierdlem51  46722  fourierdlem88  46759  fourierdlem103  46774  fourierdlem104  46775  fourierdlem107  46778  sqwvfoura  46793  sqwvfourb  46794  fouriersw  46796  elaa2lem  46798  hspmbllem1  47191  cnambpcma  47879  readdcnnred  47888  gpg3kgrtriex  48702  nn0mnd  48792  altgsumbcALT  48966  nn0sumshdiglemA  49232  line2xlem  49366  line2x  49367  itschlc0yqe  49373  itsclc0yqsollem1  49375  itschlc0xyqsol1  49379  itschlc0xyqsol  49380  2itscp  49394