Theorem addid2d 10830

Description: 0 is a left identity for addition. (Contributed by Mario Carneiro, 27-May-2016.)

Hypothesis

Ref	Expression
muld.1	⊢ (𝜑 → 𝐴 ∈ ℂ)

Assertion

Ref	Expression
addid2d	⊢ (𝜑 → (0 + 𝐴) = 𝐴)

Proof of Theorem addid2d

Step	Hyp	Ref	Expression
1		muld.1	. 2 ⊢ (𝜑 → 𝐴 ∈ ℂ)
2		addid2 10812	. 2 ⊢ (𝐴 ∈ ℂ → (0 + 𝐴) = 𝐴)
3	1, 2	syl 17	1 ⊢ (𝜑 → (0 + 𝐴) = 𝐴)

Syntax hints:   → wi 4   = wceq 1538   ∈ wcel 2111  (class class class)co 7135  ℂcc 10524  0cc0 10526   + caddc 10529

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 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2158  ax-12 2175  ax-ext 2770  ax-sep 5167  ax-nul 5174  ax-pow 5231  ax-pr 5295  ax-un 7441  ax-resscn 10583  ax-1cn 10584  ax-icn 10585  ax-addcl 10586  ax-addrcl 10587  ax-mulcl 10588  ax-mulrcl 10589  ax-mulcom 10590  ax-addass 10591  ax-mulass 10592  ax-distr 10593  ax-i2m1 10594  ax-1ne0 10595  ax-1rid 10596  ax-rnegex 10597  ax-rrecex 10598  ax-cnre 10599  ax-pre-lttri 10600  ax-pre-lttrn 10601  ax-pre-ltadd 10602

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3or 1085  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-mo 2598  df-eu 2629  df-clab 2777  df-cleq 2791  df-clel 2870  df-nfc 2938  df-ne 2988  df-nel 3092  df-ral 3111  df-rex 3112  df-rab 3115  df-v 3443  df-sbc 3721  df-csb 3829  df-dif 3884  df-un 3886  df-in 3888  df-ss 3898  df-nul 4244  df-if 4426  df-pw 4499  df-sn 4526  df-pr 4528  df-op 4532  df-uni 4801  df-br 5031  df-opab 5093  df-mpt 5111  df-id 5425  df-po 5438  df-so 5439  df-xp 5525  df-rel 5526  df-cnv 5527  df-co 5528  df-dm 5529  df-rn 5530  df-res 5531  df-ima 5532  df-iota 6283  df-fun 6326  df-fn 6327  df-f 6328  df-f1 6329  df-fo 6330  df-f1o 6331  df-fv 6332  df-ov 7138  df-er 8272  df-en 8493  df-dom 8494  df-sdom 8495  df-pnf 10666  df-mnf 10667  df-ltxr 10669

This theorem is referenced by:  negeu  10865  subge0  11142  sublt0d  11255  un0addcl  11918  lincmb01cmp  12873  ico01fl0  13184  discr  13597  ccatlid  13931  swrdfv0  14002  swrdpfx  14060  pfxpfx  14061  cats1un  14074  swrdccatin2  14082  cshwidx0mod  14158  cshw1  14175  relexpaddg  14404  rennim  14590  max0add  14662  fsumsplit  15089  sumsplit  15115  isumsplit  15187  arisum2  15208  binomfallfaclem2  15386  efaddlem  15438  eftlub  15454  ef4p  15458  rpnnen2lem11  15569  moddvds  15610  divalglem9  15742  sadadd2lem2  15789  sadcaddlem  15796  gcdmultipled  15872  pcmpt  16218  4sqlem11  16281  vdwlem6  16312  gsumsgrpccat  17996  gsumccatOLD  17997  mulgnn0dir  18249  sylow1lem1  18715  efgsval2  18851  efgsp1  18855  zaddablx  18985  pgpfaclem1  19196  regsumfsum  20159  regsumsupp  20311  mplcoe5  20708  nrmmetd  23181  blcvx  23403  xrsxmet  23414  reparphti  23602  nulmbl  24139  itg2splitlem  24352  itg2split  24353  itg2monolem1  24354  itgsplitioo  24441  ditgsplit  24464  dvcnp2  24523  dvcmul  24547  dvcmulf  24548  dvmptcmul  24567  dveflem  24582  dvef  24583  dvlipcn  24597  dvlt0  24608  plymullem1  24811  coeeulem  24821  dgradd2  24865  dgrmulc  24868  plydivlem3  24891  aareccl  24922  taylthlem1  24968  sin2kpi  25076  cos2kpi  25077  coshalfpim  25088  sinkpi  25114  chordthmlem3  25420  chordthmlem5  25422  dcubic1lem  25429  dcubic  25432  atancj  25496  atanlogaddlem  25499  atanlogsublem  25501  scvxcvx  25571  zetacvg  25600  ftalem5  25662  ftalem7  25664  basellem3  25668  chtublem  25795  2sqn0  26018  2sqnn  26023  rplogsumlem2  26069  dchrisumlem1  26073  pntrlog2bndlem2  26162  brbtwn2  26699  axlowdimlem16  26751  axeuclidlem  26756  elntg2  26779  eucrct2eupth  28030  2clwwlk2clwwlk  28135  bcm1n  30544  wrdt2ind  30653  esumpfinvallem  31443  signsplypnf  31930  fsum2dsub  31988  logdivsqrle  32031  revpfxsfxrev  32475  cvxpconn  32602  cvxsconn  32603  fwddifnp1  33739  tan2h  35049  poimirlem16  35073  mbfposadd  35104  itg2addnc  35111  ftc1anclem5  35134  bfplem2  35261  dffltz  39615  3cubeslem3r  39628  pellexlem6  39775  jm2.18  39929  sqrtcval  40341  relexpaddss  40419  int-add02d  40891  sub2times  41905  fzisoeu  41932  xralrple2  41986  cosknegpi  42511  dvsinax  42555  dvasinbx  42562  dvnxpaek  42584  dvnmul  42585  stoweidlem1  42643  stoweidlem13  42655  stoweidlem42  42684  stirlinglem5  42720  stirlinglem11  42726  fourierdlem42  42791  fourierdlem51  42799  fourierdlem88  42836  fourierdlem103  42851  fourierdlem104  42852  fourierdlem107  42855  sqwvfoura  42870  sqwvfourb  42871  fouriersw  42873  elaa2lem  42875  hspmbllem1  43265  cnambpcma  43851  readdcnnred  43860  nn0mnd  44439  altgsumbcALT  44755  nn0sumshdiglemA  45033  line2xlem  45167  line2x  45168  itschlc0yqe  45174  itsclc0yqsollem1  45176  itschlc0xyqsol1  45180  itschlc0xyqsol  45181  2itscp  45195