Theorem addlidd 11382

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

Syntax hints:   → wi 4   = wceq 1540   ∈ wcel 2109  (class class class)co 7390  ℂcc 11073  0cc0 11075   + caddc 11078

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 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2702  ax-sep 5254  ax-nul 5264  ax-pow 5323  ax-pr 5390  ax-un 7714  ax-resscn 11132  ax-1cn 11133  ax-icn 11134  ax-addcl 11135  ax-addrcl 11136  ax-mulcl 11137  ax-mulrcl 11138  ax-mulcom 11139  ax-addass 11140  ax-mulass 11141  ax-distr 11142  ax-i2m1 11143  ax-1ne0 11144  ax-1rid 11145  ax-rnegex 11146  ax-rrecex 11147  ax-cnre 11148  ax-pre-lttri 11149  ax-pre-lttrn 11150  ax-pre-ltadd 11151

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2534  df-eu 2563  df-clab 2709  df-cleq 2722  df-clel 2804  df-nfc 2879  df-ne 2927  df-nel 3031  df-ral 3046  df-rex 3055  df-rab 3409  df-v 3452  df-sbc 3757  df-csb 3866  df-dif 3920  df-un 3922  df-in 3924  df-ss 3934  df-nul 4300  df-if 4492  df-pw 4568  df-sn 4593  df-pr 4595  df-op 4599  df-uni 4875  df-br 5111  df-opab 5173  df-mpt 5192  df-id 5536  df-po 5549  df-so 5550  df-xp 5647  df-rel 5648  df-cnv 5649  df-co 5650  df-dm 5651  df-rn 5652  df-res 5653  df-ima 5654  df-iota 6467  df-fun 6516  df-fn 6517  df-f 6518  df-f1 6519  df-fo 6520  df-f1o 6521  df-fv 6522  df-ov 7393  df-er 8674  df-en 8922  df-dom 8923  df-sdom 8924  df-pnf 11217  df-mnf 11218  df-ltxr 11220

This theorem is referenced by:  negeu  11418  subge0  11698  sublt0d  11811  un0addcl  12482  lincmb01cmp  13463  ico01fl0  13788  muladdmod  13884  discr  14212  ccatlid  14558  swrdfv0  14621  swrdpfx  14679  pfxpfx  14680  cats1un  14693  swrdccatin2  14701  cshwidx0mod  14777  cshw1  14794  relexpaddg  15026  rennim  15212  max0add  15283  fsumsplit  15714  sumsplit  15741  isumsplit  15813  arisum2  15834  binomfallfaclem2  16013  efaddlem  16066  eftlub  16084  ef4p  16088  rpnnen2lem11  16199  moddvds  16240  divalglem9  16378  sadadd2lem2  16427  sadcaddlem  16434  gcdmultipled  16511  pcmpt  16870  4sqlem11  16933  vdwlem6  16964  gsumsgrpccat  18774  mulgnn0dir  19043  sylow1lem1  19535  efgsval2  19670  efgsp1  19674  zaddablx  19809  pgpfaclem1  20020  regsumfsum  21359  regsumsupp  21538  mplcoe5  21954  nrmmetd  24469  blcvx  24693  xrsxmet  24705  reparphti  24903  reparphtiOLD  24904  nulmbl  25443  itg2splitlem  25656  itg2split  25657  itg2monolem1  25658  itgsplitioo  25746  ditgsplit  25769  dvcnp2  25828  dvcnp2OLD  25829  dvcmul  25854  dvcmulf  25855  dvmptcmul  25875  dveflem  25890  dvef  25891  dvlipcn  25906  dvlt0  25917  plymullem1  26126  coeeulem  26136  dgradd2  26181  dgrmulc  26184  plydivlem3  26210  aareccl  26241  taylthlem1  26288  sin2kpi  26399  cos2kpi  26400  coshalfpim  26411  sinkpi  26438  chordthmlem3  26751  chordthmlem5  26753  dcubic1lem  26760  dcubic  26763  atancj  26827  atanlogaddlem  26830  atanlogsublem  26832  scvxcvx  26903  zetacvg  26932  ftalem5  26994  ftalem7  26996  basellem3  27000  chtublem  27129  2sqn0  27352  2sqnn  27357  rplogsumlem2  27403  dchrisumlem1  27407  pntrlog2bndlem2  27496  brbtwn2  28839  axlowdimlem16  28891  axeuclidlem  28896  elntg2  28919  eucrct2eupth  30181  2clwwlk2clwwlk  30286  re0cj  32674  bcm1n  32725  wrdt2ind  32882  nn0constr  33758  constraddcl  33759  constrnegcl  33760  constrdircl  33762  constrremulcl  33764  constrrecl  33766  constrimcl  33767  constrmulcl  33768  constrreinvcl  33769  constrinvcl  33770  constrresqrtcl  33774  constrabscl  33775  2sqr3minply  33777  cos9thpiminplylem1  33779  cos9thpiminply  33785  cos9thpinconstrlem1  33786  esumpfinvallem  34071  signsplypnf  34548  fsum2dsub  34605  logdivsqrle  34648  revpfxsfxrev  35110  cvxpconn  35236  cvxsconn  35237  fwddifnp1  36160  tan2h  37613  poimirlem16  37637  mbfposadd  37668  itg2addnc  37675  ftc1anclem5  37698  bfplem2  37824  aks4d1p1p4  42066  aks4d1p7d1  42077  primrootspoweq0  42101  aks6d1c1  42111  aks6d1c5lem1  42131  sticksstones10  42150  sticksstones22  42163  bcle2d  42174  dffltz  42629  3cubeslem3r  42682  pellexlem6  42829  jm2.18  42984  sqrtcval  43637  relexpaddss  43714  int-add02d  44181  sub2times  45278  fzisoeu  45305  xralrple2  45357  cosknegpi  45874  dvsinax  45918  dvasinbx  45925  dvnxpaek  45947  dvnmul  45948  stoweidlem1  46006  stoweidlem13  46018  stoweidlem42  46047  stirlinglem5  46083  stirlinglem11  46089  fourierdlem42  46154  fourierdlem51  46162  fourierdlem88  46199  fourierdlem103  46214  fourierdlem104  46215  fourierdlem107  46218  sqwvfoura  46233  sqwvfourb  46234  fouriersw  46236  elaa2lem  46238  hspmbllem1  46631  cnambpcma  47299  readdcnnred  47308  gpg3kgrtriex  48084  nn0mnd  48171  altgsumbcALT  48345  nn0sumshdiglemA  48612  line2xlem  48746  line2x  48747  itschlc0yqe  48753  itsclc0yqsollem1  48755  itschlc0xyqsol1  48759  itschlc0xyqsol  48760  2itscp  48774