Theorem addid2d 10912

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

Syntax hints:   → wi 4   = wceq 1542   ∈ wcel 2113  (class class class)co 7164  ℂcc 10606  0cc0 10608   + caddc 10611

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1916  ax-6 1974  ax-7 2019  ax-8 2115  ax-9 2123  ax-10 2144  ax-11 2161  ax-12 2178  ax-ext 2710  ax-sep 5164  ax-nul 5171  ax-pow 5229  ax-pr 5293  ax-un 7473  ax-resscn 10665  ax-1cn 10666  ax-icn 10667  ax-addcl 10668  ax-addrcl 10669  ax-mulcl 10670  ax-mulrcl 10671  ax-mulcom 10672  ax-addass 10673  ax-mulass 10674  ax-distr 10675  ax-i2m1 10676  ax-1ne0 10677  ax-1rid 10678  ax-rnegex 10679  ax-rrecex 10680  ax-cnre 10681  ax-pre-lttri 10682  ax-pre-lttrn 10683  ax-pre-ltadd 10684

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 847  df-3or 1089  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1787  df-nf 1791  df-sb 2074  df-mo 2540  df-eu 2570  df-clab 2717  df-cleq 2730  df-clel 2811  df-nfc 2881  df-ne 2935  df-nel 3039  df-ral 3058  df-rex 3059  df-rab 3062  df-v 3399  df-sbc 3680  df-csb 3789  df-dif 3844  df-un 3846  df-in 3848  df-ss 3858  df-nul 4210  df-if 4412  df-pw 4487  df-sn 4514  df-pr 4516  df-op 4520  df-uni 4794  df-br 5028  df-opab 5090  df-mpt 5108  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 6291  df-fun 6335  df-fn 6336  df-f 6337  df-f1 6338  df-fo 6339  df-f1o 6340  df-fv 6341  df-ov 7167  df-er 8313  df-en 8549  df-dom 8550  df-sdom 8551  df-pnf 10748  df-mnf 10749  df-ltxr 10751

This theorem is referenced by:  negeu  10947  subge0  11224  sublt0d  11337  un0addcl  12002  lincmb01cmp  12962  ico01fl0  13273  discr  13686  ccatlid  14022  swrdfv0  14093  swrdpfx  14151  pfxpfx  14152  cats1un  14165  swrdccatin2  14173  cshwidx0mod  14249  cshw1  14266  relexpaddg  14495  rennim  14681  max0add  14753  fsumsplit  15183  sumsplit  15209  isumsplit  15281  arisum2  15302  binomfallfaclem2  15479  efaddlem  15531  eftlub  15547  ef4p  15551  rpnnen2lem11  15662  moddvds  15703  divalglem9  15839  sadadd2lem2  15886  sadcaddlem  15893  gcdmultipled  15971  pcmpt  16321  4sqlem11  16384  vdwlem6  16415  gsumsgrpccat  18113  gsumccatOLD  18114  mulgnn0dir  18368  sylow1lem1  18834  efgsval2  18970  efgsp1  18974  zaddablx  19104  pgpfaclem1  19315  regsumfsum  20278  regsumsupp  20431  mplcoe5  20844  nrmmetd  23320  blcvx  23543  xrsxmet  23554  reparphti  23742  nulmbl  24280  itg2splitlem  24493  itg2split  24494  itg2monolem1  24495  itgsplitioo  24582  ditgsplit  24605  dvcnp2  24664  dvcmul  24688  dvcmulf  24689  dvmptcmul  24708  dveflem  24723  dvef  24724  dvlipcn  24738  dvlt0  24749  plymullem1  24955  coeeulem  24965  dgradd2  25009  dgrmulc  25012  plydivlem3  25035  aareccl  25066  taylthlem1  25112  sin2kpi  25220  cos2kpi  25221  coshalfpim  25232  sinkpi  25258  chordthmlem3  25564  chordthmlem5  25566  dcubic1lem  25573  dcubic  25576  atancj  25640  atanlogaddlem  25643  atanlogsublem  25645  scvxcvx  25715  zetacvg  25744  ftalem5  25806  ftalem7  25808  basellem3  25812  chtublem  25939  2sqn0  26162  2sqnn  26167  rplogsumlem2  26213  dchrisumlem1  26217  pntrlog2bndlem2  26306  brbtwn2  26843  axlowdimlem16  26895  axeuclidlem  26900  elntg2  26923  eucrct2eupth  28174  2clwwlk2clwwlk  28279  bcm1n  30683  wrdt2ind  30792  esumpfinvallem  31604  signsplypnf  32091  fsum2dsub  32149  logdivsqrle  32192  revpfxsfxrev  32640  cvxpconn  32767  cvxsconn  32768  fwddifnp1  34097  tan2h  35381  poimirlem16  35405  mbfposadd  35436  itg2addnc  35443  ftc1anclem5  35466  bfplem2  35593  aks4d1p1p4  39687  dffltz  40027  3cubeslem3r  40065  pellexlem6  40212  jm2.18  40366  sqrtcval  40778  relexpaddss  40856  int-add02d  41327  sub2times  42334  fzisoeu  42361  xralrple2  42415  cosknegpi  42936  dvsinax  42980  dvasinbx  42987  dvnxpaek  43009  dvnmul  43010  stoweidlem1  43068  stoweidlem13  43080  stoweidlem42  43109  stirlinglem5  43145  stirlinglem11  43151  fourierdlem42  43216  fourierdlem51  43224  fourierdlem88  43261  fourierdlem103  43276  fourierdlem104  43277  fourierdlem107  43280  sqwvfoura  43295  sqwvfourb  43296  fouriersw  43298  elaa2lem  43300  hspmbllem1  43690  cnambpcma  44304  readdcnnred  44313  nn0mnd  44891  altgsumbcALT  45207  nn0sumshdiglemA  45483  line2xlem  45617  line2x  45618  itschlc0yqe  45624  itsclc0yqsollem1  45626  itschlc0xyqsol1  45630  itschlc0xyqsol  45631  2itscp  45645