Theorem addlidd 11335

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

Syntax hints:   → wi 4   = wceq 1542   ∈ wcel 2114  (class class class)co 7358  ℂcc 11025  0cc0 11027   + caddc 11030

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2709  ax-sep 5231  ax-nul 5241  ax-pow 5300  ax-pr 5368  ax-un 7680  ax-resscn 11084  ax-1cn 11085  ax-icn 11086  ax-addcl 11087  ax-addrcl 11088  ax-mulcl 11089  ax-mulrcl 11090  ax-mulcom 11091  ax-addass 11092  ax-mulass 11093  ax-distr 11094  ax-i2m1 11095  ax-1ne0 11096  ax-1rid 11097  ax-rnegex 11098  ax-rrecex 11099  ax-cnre 11100  ax-pre-lttri 11101  ax-pre-lttrn 11102  ax-pre-ltadd 11103

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2540  df-eu 2570  df-clab 2716  df-cleq 2729  df-clel 2812  df-nfc 2886  df-ne 2934  df-nel 3038  df-ral 3053  df-rex 3063  df-rab 3391  df-v 3432  df-sbc 3730  df-csb 3839  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-nul 4275  df-if 4468  df-pw 4544  df-sn 4569  df-pr 4571  df-op 4575  df-uni 4852  df-br 5087  df-opab 5149  df-mpt 5168  df-id 5517  df-po 5530  df-so 5531  df-xp 5628  df-rel 5629  df-cnv 5630  df-co 5631  df-dm 5632  df-rn 5633  df-res 5634  df-ima 5635  df-iota 6446  df-fun 6492  df-fn 6493  df-f 6494  df-f1 6495  df-fo 6496  df-f1o 6497  df-fv 6498  df-ov 7361  df-er 8634  df-en 8885  df-dom 8886  df-sdom 8887  df-pnf 11169  df-mnf 11170  df-ltxr 11172

This theorem is referenced by:  negeu  11371  subge0  11651  sublt0d  11764  un0addcl  12435  lincmb01cmp  13412  ico01fl0  13740  muladdmod  13836  discr  14164  ccatlid  14511  swrdfv0  14574  swrdpfx  14631  pfxpfx  14632  cats1un  14645  swrdccatin2  14653  cshwidx0mod  14729  cshw1  14746  relexpaddg  14977  rennim  15163  max0add  15234  fsumsplit  15665  sumsplit  15692  isumsplit  15764  arisum2  15785  binomfallfaclem2  15964  efaddlem  16017  eftlub  16035  ef4p  16039  rpnnen2lem11  16150  moddvds  16191  divalglem9  16329  sadadd2lem2  16378  sadcaddlem  16385  gcdmultipled  16462  pcmpt  16821  4sqlem11  16884  vdwlem6  16915  gsumsgrpccat  18766  mulgnn0dir  19038  sylow1lem1  19531  efgsval2  19666  efgsp1  19670  zaddablx  19805  pgpfaclem1  20016  regsumfsum  21392  regsumsupp  21579  mplcoe5  21996  nrmmetd  24517  blcvx  24741  xrsxmet  24753  reparphti  24942  nulmbl  25480  itg2splitlem  25693  itg2split  25694  itg2monolem1  25695  itgsplitioo  25783  ditgsplit  25806  dvcnp2  25865  dvcmul  25889  dvcmulf  25890  dvmptcmul  25909  dveflem  25924  dvef  25925  dvlipcn  25940  dvlt0  25951  plymullem1  26160  coeeulem  26170  dgradd2  26214  dgrmulc  26217  plydivlem3  26243  aareccl  26274  taylthlem1  26321  sin2kpi  26432  cos2kpi  26433  coshalfpim  26444  sinkpi  26471  chordthmlem3  26784  chordthmlem5  26786  dcubic1lem  26793  dcubic  26796  atancj  26860  atanlogaddlem  26863  atanlogsublem  26865  scvxcvx  26936  zetacvg  26965  ftalem5  27027  ftalem7  27029  basellem3  27033  chtublem  27162  2sqn0  27385  2sqnn  27390  rplogsumlem2  27436  dchrisumlem1  27440  pntrlog2bndlem2  27529  brbtwn2  28962  axlowdimlem16  29014  axeuclidlem  29019  elntg2  29042  eucrct2eupth  30304  2clwwlk2clwwlk  30409  re0cj  32806  bcm1n  32858  wrdt2ind  33018  nn0constr  33911  constraddcl  33912  constrnegcl  33913  constrdircl  33915  constrremulcl  33917  constrrecl  33919  constrimcl  33920  constrmulcl  33921  constrreinvcl  33922  constrinvcl  33923  constrresqrtcl  33927  constrabscl  33928  2sqr3minply  33930  cos9thpiminplylem1  33932  cos9thpiminply  33938  cos9thpinconstrlem1  33939  esumpfinvallem  34224  signsplypnf  34700  fsum2dsub  34757  logdivsqrle  34800  revpfxsfxrev  35304  cvxpconn  35430  cvxsconn  35431  fwddifnp1  36353  tan2h  37924  poimirlem16  37948  mbfposadd  37979  itg2addnc  37986  ftc1anclem5  38009  bfplem2  38135  aks4d1p1p4  42502  aks4d1p7d1  42513  primrootspoweq0  42537  aks6d1c1  42547  aks6d1c5lem1  42567  sticksstones10  42586  sticksstones22  42599  bcle2d  42610  dffltz  43066  3cubeslem3r  43118  pellexlem6  43265  jm2.18  43419  sqrtcval  44071  relexpaddss  44148  int-add02d  44615  sub2times  45709  fzisoeu  45736  xralrple2  45787  cosknegpi  46301  dvsinax  46345  dvasinbx  46352  dvnxpaek  46374  dvnmul  46375  stoweidlem1  46433  stoweidlem13  46445  stoweidlem42  46474  stirlinglem5  46510  stirlinglem11  46516  fourierdlem42  46581  fourierdlem51  46589  fourierdlem88  46626  fourierdlem103  46641  fourierdlem104  46642  fourierdlem107  46645  sqwvfoura  46660  sqwvfourb  46661  fouriersw  46663  elaa2lem  46665  hspmbllem1  47058  cnambpcma  47728  readdcnnred  47737  gpg3kgrtriex  48523  nn0mnd  48613  altgsumbcALT  48787  nn0sumshdiglemA  49053  line2xlem  49187  line2x  49188  itschlc0yqe  49194  itsclc0yqsollem1  49196  itschlc0xyqsol1  49200  itschlc0xyqsol  49201  2itscp  49215