Theorem addlidd 11462

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

Syntax hints:   → wi 4   = wceq 1540   ∈ wcel 2108  (class class class)co 7431  ℂcc 11153  0cc0 11155   + caddc 11158

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2157  ax-12 2177  ax-ext 2708  ax-sep 5296  ax-nul 5306  ax-pow 5365  ax-pr 5432  ax-un 7755  ax-resscn 11212  ax-1cn 11213  ax-icn 11214  ax-addcl 11215  ax-addrcl 11216  ax-mulcl 11217  ax-mulrcl 11218  ax-mulcom 11219  ax-addass 11220  ax-mulass 11221  ax-distr 11222  ax-i2m1 11223  ax-1ne0 11224  ax-1rid 11225  ax-rnegex 11226  ax-rrecex 11227  ax-cnre 11228  ax-pre-lttri 11229  ax-pre-lttrn 11230  ax-pre-ltadd 11231

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2065  df-mo 2540  df-eu 2569  df-clab 2715  df-cleq 2729  df-clel 2816  df-nfc 2892  df-ne 2941  df-nel 3047  df-ral 3062  df-rex 3071  df-rab 3437  df-v 3482  df-sbc 3789  df-csb 3900  df-dif 3954  df-un 3956  df-in 3958  df-ss 3968  df-nul 4334  df-if 4526  df-pw 4602  df-sn 4627  df-pr 4629  df-op 4633  df-uni 4908  df-br 5144  df-opab 5206  df-mpt 5226  df-id 5578  df-po 5592  df-so 5593  df-xp 5691  df-rel 5692  df-cnv 5693  df-co 5694  df-dm 5695  df-rn 5696  df-res 5697  df-ima 5698  df-iota 6514  df-fun 6563  df-fn 6564  df-f 6565  df-f1 6566  df-fo 6567  df-f1o 6568  df-fv 6569  df-ov 7434  df-er 8745  df-en 8986  df-dom 8987  df-sdom 8988  df-pnf 11297  df-mnf 11298  df-ltxr 11300

This theorem is referenced by:  negeu  11498  subge0  11776  sublt0d  11889  un0addcl  12559  lincmb01cmp  13535  ico01fl0  13859  muladdmod  13953  discr  14279  ccatlid  14624  swrdfv0  14687  swrdpfx  14745  pfxpfx  14746  cats1un  14759  swrdccatin2  14767  cshwidx0mod  14843  cshw1  14860  relexpaddg  15092  rennim  15278  max0add  15349  fsumsplit  15777  sumsplit  15804  isumsplit  15876  arisum2  15897  binomfallfaclem2  16076  efaddlem  16129  eftlub  16145  ef4p  16149  rpnnen2lem11  16260  moddvds  16301  divalglem9  16438  sadadd2lem2  16487  sadcaddlem  16494  gcdmultipled  16571  pcmpt  16930  4sqlem11  16993  vdwlem6  17024  gsumsgrpccat  18853  mulgnn0dir  19122  sylow1lem1  19616  efgsval2  19751  efgsp1  19755  zaddablx  19890  pgpfaclem1  20101  regsumfsum  21453  regsumsupp  21640  mplcoe5  22058  nrmmetd  24587  blcvx  24819  xrsxmet  24831  reparphti  25029  reparphtiOLD  25030  nulmbl  25570  itg2splitlem  25783  itg2split  25784  itg2monolem1  25785  itgsplitioo  25873  ditgsplit  25896  dvcnp2  25955  dvcnp2OLD  25956  dvcmul  25981  dvcmulf  25982  dvmptcmul  26002  dveflem  26017  dvef  26018  dvlipcn  26033  dvlt0  26044  plymullem1  26253  coeeulem  26263  dgradd2  26308  dgrmulc  26311  plydivlem3  26337  aareccl  26368  taylthlem1  26415  sin2kpi  26525  cos2kpi  26526  coshalfpim  26537  sinkpi  26564  chordthmlem3  26877  chordthmlem5  26879  dcubic1lem  26886  dcubic  26889  atancj  26953  atanlogaddlem  26956  atanlogsublem  26958  scvxcvx  27029  zetacvg  27058  ftalem5  27120  ftalem7  27122  basellem3  27126  chtublem  27255  2sqn0  27478  2sqnn  27483  rplogsumlem2  27529  dchrisumlem1  27533  pntrlog2bndlem2  27622  brbtwn2  28920  axlowdimlem16  28972  axeuclidlem  28977  elntg2  29000  eucrct2eupth  30264  2clwwlk2clwwlk  30369  re0cj  32753  bcm1n  32797  wrdt2ind  32938  2sqr3minply  33791  esumpfinvallem  34075  signsplypnf  34565  fsum2dsub  34622  logdivsqrle  34665  revpfxsfxrev  35121  cvxpconn  35247  cvxsconn  35248  fwddifnp1  36166  tan2h  37619  poimirlem16  37643  mbfposadd  37674  itg2addnc  37681  ftc1anclem5  37704  bfplem2  37830  aks4d1p1p4  42072  aks4d1p7d1  42083  primrootspoweq0  42107  aks6d1c1  42117  aks6d1c5lem1  42137  sticksstones10  42156  sticksstones22  42169  bcle2d  42180  dffltz  42644  3cubeslem3r  42698  pellexlem6  42845  jm2.18  43000  sqrtcval  43654  relexpaddss  43731  int-add02d  44198  sub2times  45284  fzisoeu  45312  xralrple2  45365  cosknegpi  45884  dvsinax  45928  dvasinbx  45935  dvnxpaek  45957  dvnmul  45958  stoweidlem1  46016  stoweidlem13  46028  stoweidlem42  46057  stirlinglem5  46093  stirlinglem11  46099  fourierdlem42  46164  fourierdlem51  46172  fourierdlem88  46209  fourierdlem103  46224  fourierdlem104  46225  fourierdlem107  46228  sqwvfoura  46243  sqwvfourb  46244  fouriersw  46246  elaa2lem  46248  hspmbllem1  46641  cnambpcma  47306  readdcnnred  47315  gpg3kgrtriex  48045  nn0mnd  48095  altgsumbcALT  48269  nn0sumshdiglemA  48540  line2xlem  48674  line2x  48675  itschlc0yqe  48681  itsclc0yqsollem1  48683  itschlc0xyqsol1  48687  itschlc0xyqsol  48688  2itscp  48702