Theorem addlidd 11320

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

Syntax hints:   → wi 4   = wceq 1541   ∈ wcel 2111  (class class class)co 7352  ℂcc 11010  0cc0 11012   + caddc 11015

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-10 2144  ax-11 2160  ax-12 2180  ax-ext 2703  ax-sep 5236  ax-nul 5246  ax-pow 5305  ax-pr 5372  ax-un 7674  ax-resscn 11069  ax-1cn 11070  ax-icn 11071  ax-addcl 11072  ax-addrcl 11073  ax-mulcl 11074  ax-mulrcl 11075  ax-mulcom 11076  ax-addass 11077  ax-mulass 11078  ax-distr 11079  ax-i2m1 11080  ax-1ne0 11081  ax-1rid 11082  ax-rnegex 11083  ax-rrecex 11084  ax-cnre 11085  ax-pre-lttri 11086  ax-pre-lttrn 11087  ax-pre-ltadd 11088

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-nf 1785  df-sb 2068  df-mo 2535  df-eu 2564  df-clab 2710  df-cleq 2723  df-clel 2806  df-nfc 2881  df-ne 2929  df-nel 3033  df-ral 3048  df-rex 3057  df-rab 3396  df-v 3438  df-sbc 3737  df-csb 3846  df-dif 3900  df-un 3902  df-in 3904  df-ss 3914  df-nul 4283  df-if 4475  df-pw 4551  df-sn 4576  df-pr 4578  df-op 4582  df-uni 4859  df-br 5094  df-opab 5156  df-mpt 5175  df-id 5514  df-po 5527  df-so 5528  df-xp 5625  df-rel 5626  df-cnv 5627  df-co 5628  df-dm 5629  df-rn 5630  df-res 5631  df-ima 5632  df-iota 6443  df-fun 6489  df-fn 6490  df-f 6491  df-f1 6492  df-fo 6493  df-f1o 6494  df-fv 6495  df-ov 7355  df-er 8628  df-en 8876  df-dom 8877  df-sdom 8878  df-pnf 11154  df-mnf 11155  df-ltxr 11157

This theorem is referenced by:  negeu  11356  subge0  11636  sublt0d  11749  un0addcl  12420  lincmb01cmp  13401  ico01fl0  13729  muladdmod  13825  discr  14153  ccatlid  14500  swrdfv0  14563  swrdpfx  14620  pfxpfx  14621  cats1un  14634  swrdccatin2  14642  cshwidx0mod  14718  cshw1  14735  relexpaddg  14966  rennim  15152  max0add  15223  fsumsplit  15654  sumsplit  15681  isumsplit  15753  arisum2  15774  binomfallfaclem2  15953  efaddlem  16006  eftlub  16024  ef4p  16028  rpnnen2lem11  16139  moddvds  16180  divalglem9  16318  sadadd2lem2  16367  sadcaddlem  16374  gcdmultipled  16451  pcmpt  16810  4sqlem11  16873  vdwlem6  16904  gsumsgrpccat  18754  mulgnn0dir  19023  sylow1lem1  19516  efgsval2  19651  efgsp1  19655  zaddablx  19790  pgpfaclem1  20001  regsumfsum  21378  regsumsupp  21565  mplcoe5  21981  nrmmetd  24495  blcvx  24719  xrsxmet  24731  reparphti  24929  reparphtiOLD  24930  nulmbl  25469  itg2splitlem  25682  itg2split  25683  itg2monolem1  25684  itgsplitioo  25772  ditgsplit  25795  dvcnp2  25854  dvcnp2OLD  25855  dvcmul  25880  dvcmulf  25881  dvmptcmul  25901  dveflem  25916  dvef  25917  dvlipcn  25932  dvlt0  25943  plymullem1  26152  coeeulem  26162  dgradd2  26207  dgrmulc  26210  plydivlem3  26236  aareccl  26267  taylthlem1  26314  sin2kpi  26425  cos2kpi  26426  coshalfpim  26437  sinkpi  26464  chordthmlem3  26777  chordthmlem5  26779  dcubic1lem  26786  dcubic  26789  atancj  26853  atanlogaddlem  26856  atanlogsublem  26858  scvxcvx  26929  zetacvg  26958  ftalem5  27020  ftalem7  27022  basellem3  27026  chtublem  27155  2sqn0  27378  2sqnn  27383  rplogsumlem2  27429  dchrisumlem1  27433  pntrlog2bndlem2  27522  brbtwn2  28890  axlowdimlem16  28942  axeuclidlem  28947  elntg2  28970  eucrct2eupth  30232  2clwwlk2clwwlk  30337  re0cj  32734  bcm1n  32784  wrdt2ind  32941  nn0constr  33781  constraddcl  33782  constrnegcl  33783  constrdircl  33785  constrremulcl  33787  constrrecl  33789  constrimcl  33790  constrmulcl  33791  constrreinvcl  33792  constrinvcl  33793  constrresqrtcl  33797  constrabscl  33798  2sqr3minply  33800  cos9thpiminplylem1  33802  cos9thpiminply  33808  cos9thpinconstrlem1  33809  esumpfinvallem  34094  signsplypnf  34570  fsum2dsub  34627  logdivsqrle  34670  revpfxsfxrev  35167  cvxpconn  35293  cvxsconn  35294  fwddifnp1  36216  tan2h  37658  poimirlem16  37682  mbfposadd  37713  itg2addnc  37720  ftc1anclem5  37743  bfplem2  37869  aks4d1p1p4  42170  aks4d1p7d1  42181  primrootspoweq0  42205  aks6d1c1  42215  aks6d1c5lem1  42235  sticksstones10  42254  sticksstones22  42267  bcle2d  42278  dffltz  42733  3cubeslem3r  42785  pellexlem6  42932  jm2.18  43086  sqrtcval  43739  relexpaddss  43816  int-add02d  44283  sub2times  45379  fzisoeu  45406  xralrple2  45458  cosknegpi  45972  dvsinax  46016  dvasinbx  46023  dvnxpaek  46045  dvnmul  46046  stoweidlem1  46104  stoweidlem13  46116  stoweidlem42  46145  stirlinglem5  46181  stirlinglem11  46187  fourierdlem42  46252  fourierdlem51  46260  fourierdlem88  46297  fourierdlem103  46312  fourierdlem104  46313  fourierdlem107  46316  sqwvfoura  46331  sqwvfourb  46332  fouriersw  46334  elaa2lem  46336  hspmbllem1  46729  cnambpcma  47399  readdcnnred  47408  gpg3kgrtriex  48194  nn0mnd  48284  altgsumbcALT  48458  nn0sumshdiglemA  48725  line2xlem  48859  line2x  48860  itschlc0yqe  48866  itsclc0yqsollem1  48868  itschlc0xyqsol1  48872  itschlc0xyqsol  48873  2itscp  48887