Theorem addlidd 11444

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

Syntax hints:   → wi 4   = wceq 1539   ∈ wcel 2107  (class class class)co 7413  ℂcc 11135  0cc0 11137   + caddc 11140

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-8 2109  ax-9 2117  ax-10 2140  ax-11 2156  ax-12 2176  ax-ext 2706  ax-sep 5276  ax-nul 5286  ax-pow 5345  ax-pr 5412  ax-un 7737  ax-resscn 11194  ax-1cn 11195  ax-icn 11196  ax-addcl 11197  ax-addrcl 11198  ax-mulcl 11199  ax-mulrcl 11200  ax-mulcom 11201  ax-addass 11202  ax-mulass 11203  ax-distr 11204  ax-i2m1 11205  ax-1ne0 11206  ax-1rid 11207  ax-rnegex 11208  ax-rrecex 11209  ax-cnre 11210  ax-pre-lttri 11211  ax-pre-lttrn 11212  ax-pre-ltadd 11213

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1779  df-nf 1783  df-sb 2064  df-mo 2538  df-eu 2567  df-clab 2713  df-cleq 2726  df-clel 2808  df-nfc 2884  df-ne 2932  df-nel 3036  df-ral 3051  df-rex 3060  df-rab 3420  df-v 3465  df-sbc 3771  df-csb 3880  df-dif 3934  df-un 3936  df-in 3938  df-ss 3948  df-nul 4314  df-if 4506  df-pw 4582  df-sn 4607  df-pr 4609  df-op 4613  df-uni 4888  df-br 5124  df-opab 5186  df-mpt 5206  df-id 5558  df-po 5572  df-so 5573  df-xp 5671  df-rel 5672  df-cnv 5673  df-co 5674  df-dm 5675  df-rn 5676  df-res 5677  df-ima 5678  df-iota 6494  df-fun 6543  df-fn 6544  df-f 6545  df-f1 6546  df-fo 6547  df-f1o 6548  df-fv 6549  df-ov 7416  df-er 8727  df-en 8968  df-dom 8969  df-sdom 8970  df-pnf 11279  df-mnf 11280  df-ltxr 11282

This theorem is referenced by:  negeu  11480  subge0  11758  sublt0d  11871  un0addcl  12542  lincmb01cmp  13517  ico01fl0  13841  muladdmod  13935  discr  14261  ccatlid  14606  swrdfv0  14669  swrdpfx  14727  pfxpfx  14728  cats1un  14741  swrdccatin2  14749  cshwidx0mod  14825  cshw1  14842  relexpaddg  15074  rennim  15260  max0add  15331  fsumsplit  15759  sumsplit  15786  isumsplit  15858  arisum2  15879  binomfallfaclem2  16058  efaddlem  16111  eftlub  16127  ef4p  16131  rpnnen2lem11  16242  moddvds  16283  divalglem9  16420  sadadd2lem2  16469  sadcaddlem  16476  gcdmultipled  16553  pcmpt  16912  4sqlem11  16975  vdwlem6  17006  gsumsgrpccat  18822  mulgnn0dir  19091  sylow1lem1  19584  efgsval2  19719  efgsp1  19723  zaddablx  19858  pgpfaclem1  20069  regsumfsum  21415  regsumsupp  21594  mplcoe5  22012  nrmmetd  24531  blcvx  24755  xrsxmet  24767  reparphti  24965  reparphtiOLD  24966  nulmbl  25506  itg2splitlem  25719  itg2split  25720  itg2monolem1  25721  itgsplitioo  25809  ditgsplit  25832  dvcnp2  25891  dvcnp2OLD  25892  dvcmul  25917  dvcmulf  25918  dvmptcmul  25938  dveflem  25953  dvef  25954  dvlipcn  25969  dvlt0  25980  plymullem1  26189  coeeulem  26199  dgradd2  26244  dgrmulc  26247  plydivlem3  26273  aareccl  26304  taylthlem1  26351  sin2kpi  26461  cos2kpi  26462  coshalfpim  26473  sinkpi  26500  chordthmlem3  26813  chordthmlem5  26815  dcubic1lem  26822  dcubic  26825  atancj  26889  atanlogaddlem  26892  atanlogsublem  26894  scvxcvx  26965  zetacvg  26994  ftalem5  27056  ftalem7  27058  basellem3  27062  chtublem  27191  2sqn0  27414  2sqnn  27419  rplogsumlem2  27465  dchrisumlem1  27469  pntrlog2bndlem2  27558  brbtwn2  28850  axlowdimlem16  28902  axeuclidlem  28907  elntg2  28930  eucrct2eupth  30192  2clwwlk2clwwlk  30297  re0cj  32688  bcm1n  32736  wrdt2ind  32878  nn0constr  33741  constraddcl  33742  constrnegcl  33743  constrdircl  33745  constrremulcl  33747  2sqr3minply  33749  esumpfinvallem  34034  signsplypnf  34524  fsum2dsub  34581  logdivsqrle  34624  revpfxsfxrev  35080  cvxpconn  35206  cvxsconn  35207  fwddifnp1  36125  tan2h  37578  poimirlem16  37602  mbfposadd  37633  itg2addnc  37640  ftc1anclem5  37663  bfplem2  37789  aks4d1p1p4  42031  aks4d1p7d1  42042  primrootspoweq0  42066  aks6d1c1  42076  aks6d1c5lem1  42096  sticksstones10  42115  sticksstones22  42128  bcle2d  42139  dffltz  42607  3cubeslem3r  42661  pellexlem6  42808  jm2.18  42963  sqrtcval  43616  relexpaddss  43693  int-add02d  44160  sub2times  45241  fzisoeu  45269  xralrple2  45322  cosknegpi  45841  dvsinax  45885  dvasinbx  45892  dvnxpaek  45914  dvnmul  45915  stoweidlem1  45973  stoweidlem13  45985  stoweidlem42  46014  stirlinglem5  46050  stirlinglem11  46056  fourierdlem42  46121  fourierdlem51  46129  fourierdlem88  46166  fourierdlem103  46181  fourierdlem104  46182  fourierdlem107  46185  sqwvfoura  46200  sqwvfourb  46201  fouriersw  46203  elaa2lem  46205  hspmbllem1  46598  cnambpcma  47264  readdcnnred  47273  gpg3kgrtriex  48003  nn0mnd  48053  altgsumbcALT  48227  nn0sumshdiglemA  48498  line2xlem  48632  line2x  48633  itschlc0yqe  48639  itsclc0yqsollem1  48641  itschlc0xyqsol1  48645  itschlc0xyqsol  48646  2itscp  48660