Theorem addid2d 11185

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

Syntax hints:   → wi 4   = wceq 1539   ∈ wcel 2107  (class class class)co 7284  ℂcc 10878  0cc0 10880   + caddc 10883

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2710  ax-sep 5224  ax-nul 5231  ax-pow 5289  ax-pr 5353  ax-un 7597  ax-resscn 10937  ax-1cn 10938  ax-icn 10939  ax-addcl 10940  ax-addrcl 10941  ax-mulcl 10942  ax-mulrcl 10943  ax-mulcom 10944  ax-addass 10945  ax-mulass 10946  ax-distr 10947  ax-i2m1 10948  ax-1ne0 10949  ax-1rid 10950  ax-rnegex 10951  ax-rrecex 10952  ax-cnre 10953  ax-pre-lttri 10954  ax-pre-lttrn 10955  ax-pre-ltadd 10956

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3or 1087  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2541  df-eu 2570  df-clab 2717  df-cleq 2731  df-clel 2817  df-nfc 2890  df-ne 2945  df-nel 3051  df-ral 3070  df-rex 3071  df-rab 3074  df-v 3435  df-sbc 3718  df-csb 3834  df-dif 3891  df-un 3893  df-in 3895  df-ss 3905  df-nul 4258  df-if 4461  df-pw 4536  df-sn 4563  df-pr 4565  df-op 4569  df-uni 4841  df-br 5076  df-opab 5138  df-mpt 5159  df-id 5490  df-po 5504  df-so 5505  df-xp 5596  df-rel 5597  df-cnv 5598  df-co 5599  df-dm 5600  df-rn 5601  df-res 5602  df-ima 5603  df-iota 6395  df-fun 6439  df-fn 6440  df-f 6441  df-f1 6442  df-fo 6443  df-f1o 6444  df-fv 6445  df-ov 7287  df-er 8507  df-en 8743  df-dom 8744  df-sdom 8745  df-pnf 11020  df-mnf 11021  df-ltxr 11023

This theorem is referenced by:  negeu  11220  subge0  11497  sublt0d  11610  un0addcl  12275  lincmb01cmp  13236  ico01fl0  13548  discr  13964  ccatlid  14300  swrdfv0  14371  swrdpfx  14429  pfxpfx  14430  cats1un  14443  swrdccatin2  14451  cshwidx0mod  14527  cshw1  14544  relexpaddg  14773  rennim  14959  max0add  15031  fsumsplit  15462  sumsplit  15489  isumsplit  15561  arisum2  15582  binomfallfaclem2  15759  efaddlem  15811  eftlub  15827  ef4p  15831  rpnnen2lem11  15942  moddvds  15983  divalglem9  16119  sadadd2lem2  16166  sadcaddlem  16173  gcdmultipled  16251  pcmpt  16602  4sqlem11  16665  vdwlem6  16696  gsumsgrpccat  18487  gsumccatOLD  18488  mulgnn0dir  18742  sylow1lem1  19212  efgsval2  19348  efgsp1  19352  zaddablx  19482  pgpfaclem1  19693  regsumfsum  20675  regsumsupp  20836  mplcoe5  21250  nrmmetd  23739  blcvx  23970  xrsxmet  23981  reparphti  24169  nulmbl  24708  itg2splitlem  24922  itg2split  24923  itg2monolem1  24924  itgsplitioo  25011  ditgsplit  25034  dvcnp2  25093  dvcmul  25117  dvcmulf  25118  dvmptcmul  25137  dveflem  25152  dvef  25153  dvlipcn  25167  dvlt0  25178  plymullem1  25384  coeeulem  25394  dgradd2  25438  dgrmulc  25441  plydivlem3  25464  aareccl  25495  taylthlem1  25541  sin2kpi  25649  cos2kpi  25650  coshalfpim  25661  sinkpi  25687  chordthmlem3  25993  chordthmlem5  25995  dcubic1lem  26002  dcubic  26005  atancj  26069  atanlogaddlem  26072  atanlogsublem  26074  scvxcvx  26144  zetacvg  26173  ftalem5  26235  ftalem7  26237  basellem3  26241  chtublem  26368  2sqn0  26591  2sqnn  26596  rplogsumlem2  26642  dchrisumlem1  26646  pntrlog2bndlem2  26735  brbtwn2  27282  axlowdimlem16  27334  axeuclidlem  27339  elntg2  27362  eucrct2eupth  28618  2clwwlk2clwwlk  28723  bcm1n  31125  wrdt2ind  31234  esumpfinvallem  32051  signsplypnf  32538  fsum2dsub  32596  logdivsqrle  32639  revpfxsfxrev  33086  cvxpconn  33213  cvxsconn  33214  fwddifnp1  34476  tan2h  35778  poimirlem16  35802  mbfposadd  35833  itg2addnc  35840  ftc1anclem5  35863  bfplem2  35990  aks4d1p1p4  40086  aks4d1p7d1  40097  sticksstones10  40118  sticksstones22  40131  dffltz  40478  3cubeslem3r  40516  pellexlem6  40663  jm2.18  40817  sqrtcval  41256  relexpaddss  41333  int-add02d  41803  sub2times  42820  fzisoeu  42846  xralrple2  42900  cosknegpi  43417  dvsinax  43461  dvasinbx  43468  dvnxpaek  43490  dvnmul  43491  stoweidlem1  43549  stoweidlem13  43561  stoweidlem42  43590  stirlinglem5  43626  stirlinglem11  43632  fourierdlem42  43697  fourierdlem51  43705  fourierdlem88  43742  fourierdlem103  43757  fourierdlem104  43758  fourierdlem107  43761  sqwvfoura  43776  sqwvfourb  43777  fouriersw  43779  elaa2lem  43781  hspmbllem1  44171  cnambpcma  44797  readdcnnred  44806  nn0mnd  45384  altgsumbcALT  45700  nn0sumshdiglemA  45976  line2xlem  46110  line2x  46111  itschlc0yqe  46117  itsclc0yqsollem1  46119  itschlc0xyqsol1  46123  itschlc0xyqsol  46124  2itscp  46138