Theorem addlidd 11347

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

Syntax hints:   → wi 4   = wceq 1542   ∈ wcel 2114  (class class class)co 7367  ℂcc 11036  0cc0 11038   + caddc 11041

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 5232  ax-nul 5242  ax-pow 5308  ax-pr 5376  ax-un 7689  ax-resscn 11095  ax-1cn 11096  ax-icn 11097  ax-addcl 11098  ax-addrcl 11099  ax-mulcl 11100  ax-mulrcl 11101  ax-mulcom 11102  ax-addass 11103  ax-mulass 11104  ax-distr 11105  ax-i2m1 11106  ax-1ne0 11107  ax-1rid 11108  ax-rnegex 11109  ax-rrecex 11110  ax-cnre 11111  ax-pre-lttri 11112  ax-pre-lttrn 11113  ax-pre-ltadd 11114

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 5526  df-po 5539  df-so 5540  df-xp 5637  df-rel 5638  df-cnv 5639  df-co 5640  df-dm 5641  df-rn 5642  df-res 5643  df-ima 5644  df-iota 6455  df-fun 6501  df-fn 6502  df-f 6503  df-f1 6504  df-fo 6505  df-f1o 6506  df-fv 6507  df-ov 7370  df-er 8643  df-en 8894  df-dom 8895  df-sdom 8896  df-pnf 11181  df-mnf 11182  df-ltxr 11184

This theorem is referenced by:  negeu  11383  subge0  11663  sublt0d  11776  un0addcl  12470  lincmb01cmp  13448  ico01fl0  13778  muladdmod  13874  discr  14202  ccatlid  14549  swrdfv0  14612  swrdpfx  14669  pfxpfx  14670  cats1un  14683  swrdccatin2  14691  cshwidx0mod  14767  cshw1  14784  relexpaddg  15015  rennim  15201  max0add  15272  fsumsplit  15703  sumsplit  15730  isumsplit  15805  arisum2  15826  binomfallfaclem2  16005  efaddlem  16058  eftlub  16076  ef4p  16080  rpnnen2lem11  16191  moddvds  16232  divalglem9  16370  sadadd2lem2  16419  sadcaddlem  16426  gcdmultipled  16503  pcmpt  16863  4sqlem11  16926  vdwlem6  16957  gsumsgrpccat  18808  mulgnn0dir  19080  sylow1lem1  19573  efgsval2  19708  efgsp1  19712  zaddablx  19847  pgpfaclem1  20058  regsumfsum  21415  regsumsupp  21602  mplcoe5  22018  nrmmetd  24539  blcvx  24763  xrsxmet  24775  reparphti  24964  nulmbl  25502  itg2splitlem  25715  itg2split  25716  itg2monolem1  25717  itgsplitioo  25805  ditgsplit  25828  dvcnp2  25887  dvcmul  25911  dvcmulf  25912  dvmptcmul  25931  dveflem  25946  dvef  25947  dvlipcn  25961  dvlt0  25972  plymullem1  26179  coeeulem  26189  dgradd2  26233  dgrmulc  26236  plydivlem3  26261  aareccl  26292  taylthlem1  26338  sin2kpi  26447  cos2kpi  26448  coshalfpim  26459  sinkpi  26486  chordthmlem3  26798  chordthmlem5  26800  dcubic1lem  26807  dcubic  26810  atancj  26874  atanlogaddlem  26877  atanlogsublem  26879  scvxcvx  26949  zetacvg  26978  ftalem5  27040  ftalem7  27042  basellem3  27046  chtublem  27174  2sqn0  27397  2sqnn  27402  rplogsumlem2  27448  dchrisumlem1  27452  pntrlog2bndlem2  27541  brbtwn2  28974  axlowdimlem16  29026  axeuclidlem  29031  elntg2  29054  eucrct2eupth  30315  2clwwlk2clwwlk  30420  re0cj  32816  bcm1n  32868  wrdt2ind  33013  nn0constr  33905  constraddcl  33906  constrnegcl  33907  constrdircl  33909  constrremulcl  33911  constrrecl  33913  constrimcl  33914  constrmulcl  33915  constrreinvcl  33916  constrinvcl  33917  constrresqrtcl  33921  constrabscl  33922  2sqr3minply  33924  cos9thpiminplylem1  33926  cos9thpiminply  33932  cos9thpinconstrlem1  33933  esumpfinvallem  34218  signsplypnf  34694  fsum2dsub  34751  logdivsqrle  34794  revpfxsfxrev  35298  cvxpconn  35424  cvxsconn  35425  fwddifnp1  36347  tan2h  37933  poimirlem16  37957  mbfposadd  37988  itg2addnc  37995  ftc1anclem5  38018  bfplem2  38144  aks4d1p1p4  42510  aks4d1p7d1  42521  primrootspoweq0  42545  aks6d1c1  42555  aks6d1c5lem1  42575  sticksstones10  42594  sticksstones22  42607  bcle2d  42618  dffltz  43067  3cubeslem3r  43119  pellexlem6  43262  jm2.18  43416  sqrtcval  44068  relexpaddss  44145  int-add02d  44612  sub2times  45706  fzisoeu  45733  xralrple2  45784  cosknegpi  46297  dvsinax  46341  dvasinbx  46348  dvnxpaek  46370  dvnmul  46371  stoweidlem1  46429  stoweidlem13  46441  stoweidlem42  46470  stirlinglem5  46506  stirlinglem11  46512  fourierdlem42  46577  fourierdlem51  46585  fourierdlem88  46622  fourierdlem103  46637  fourierdlem104  46638  fourierdlem107  46641  sqwvfoura  46656  sqwvfourb  46657  fouriersw  46659  elaa2lem  46661  hspmbllem1  47054  cnambpcma  47736  readdcnnred  47745  gpg3kgrtriex  48559  nn0mnd  48649  altgsumbcALT  48823  nn0sumshdiglemA  49089  line2xlem  49223  line2x  49224  itschlc0yqe  49230  itsclc0yqsollem1  49232  itschlc0xyqsol1  49236  itschlc0xyqsol  49237  2itscp  49251