Theorem addlidd 11370

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

Syntax hints:   → wi 4   = wceq 1550   ∈ wcel 2132  (class class class)co 7381  ℂcc 11057  0cc0 11059   + caddc 11062

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1805  ax-4 1819  ax-5 1920  ax-6 1977  ax-7 2018  ax-8 2134  ax-9 2142  ax-10 2165  ax-11 2181  ax-12 2202  ax-ext 2724  ax-sep 5236  ax-nul 5246  ax-pow 5312  ax-pr 5380  ax-un 7703  ax-resscn 11116  ax-1cn 11117  ax-icn 11118  ax-addcl 11119  ax-addrcl 11120  ax-mulcl 11121  ax-mulrcl 11122  ax-mulcom 11123  ax-addass 11124  ax-mulass 11125  ax-distr 11126  ax-i2m1 11127  ax-1ne0 11128  ax-1rid 11129  ax-rnegex 11130  ax-rrecex 11131  ax-cnre 11132  ax-pre-lttri 11133  ax-pre-lttrn 11134  ax-pre-ltadd 11135

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 857  df-3or 1096  df-3an 1097  df-tru 1553  df-fal 1563  df-ex 1790  df-nf 1794  df-sb 2081  df-mo 2556  df-eu 2586  df-clab 2731  df-cleq 2744  df-clel 2827  df-nfc 2901  df-ne 2948  df-nel 3052  df-ral 3067  df-rex 3077  df-rab 3405  df-v 3446  df-sbc 3736  df-csb 3844  df-dif 3898  df-un 3900  df-in 3902  df-ss 3912  df-nul 4277  df-if 4471  df-pw 4547  df-sn 4573  df-pr 4575  df-op 4579  df-uni 4856  df-br 5091  df-opab 5153  df-mpt 5172  df-id 5531  df-po 5544  df-so 5545  df-xp 5642  df-rel 5643  df-cnv 5644  df-co 5645  df-dm 5646  df-rn 5647  df-res 5648  df-ima 5649  df-iota 6462  df-fun 6508  df-fn 6509  df-f 6510  df-f1 6511  df-fo 6512  df-f1o 6513  df-fv 6514  df-ov 7384  df-er 8662  df-en 8913  df-dom 8914  df-sdom 8915  df-pnf 11204  df-mnf 11205  df-ltxr 11207

This theorem is referenced by:  negeu  11406  subge0  11686  sublt0d  11799  un0addcl  12500  lincmb01cmp  13485  ico01fl0  13815  muladdmod  13911  discr  14239  ccatlid  14586  swrdfv0  14649  swrdpfx  14706  pfxpfx  14707  cats1un  14720  swrdccatin2  14728  cshwidx0mod  14804  cshw1  14821  relexpaddg  15052  rennim  15238  max0add  15309  fsumsplit  15740  sumsplit  15767  isumsplit  15842  arisum2  15863  binomfallfaclem2  16042  efaddlem  16095  eftlub  16113  ef4p  16117  rpnnen2lem11  16228  moddvds  16269  divalglem9  16407  sadadd2lem2  16456  sadcaddlem  16463  gcdmultipled  16540  pcmpt  16900  4sqlem11  16963  vdwlem6  16994  gsumsgrpccat  18846  mulgnn0dir  19118  sylow1lem1  19610  efgsval2  19745  efgsp1  19749  zaddablx  19884  pgpfaclem1  20095  regsumfsum  21456  regsumsupp  21643  mplcoe5  22062  nrmmetd  24603  blcvx  24827  xrsxmet  24839  reparphti  25028  nulmbl  25566  itg2splitlem  25779  itg2split  25780  itg2monolem1  25781  itgsplitioo  25869  ditgsplit  25892  dvcnp2  25951  dvcmul  25975  dvcmulf  25976  dvmptcmul  25995  dveflem  26010  dvef  26011  dvlipcn  26025  dvlt0  26036  plymullem1  26243  coeeulem  26253  dgradd2  26297  dgrmulc  26300  plydivlem3  26325  aareccl  26356  taylthlem1  26402  sin2kpi  26514  cos2kpi  26515  coshalfpim  26526  sinkpi  26553  chordthmlem3  26865  chordthmlem5  26867  dcubic1lem  26874  dcubic  26877  atancj  26941  atanlogaddlem  26944  atanlogsublem  26946  scvxcvx  27016  zetacvg  27045  ftalem5  27107  ftalem7  27109  basellem3  27113  chtublem  27241  2sqn0  27464  2sqnn  27469  rplogsumlem2  27515  dchrisumlem1  27519  pntrlog2bndlem2  27608  brbtwn2  29041  axlowdimlem16  29093  axeuclidlem  29098  elntg2  29121  eucrct2eupth  30382  2clwwlk2clwwlk  30487  re0cj  32884  bcm1n  32936  wrdt2ind  33081  nn0constr  34002  constraddcl  34003  constrnegcl  34004  constrdircl  34006  constrremulcl  34008  constrrecl  34010  constrimcl  34011  constrmulcl  34012  constrreinvcl  34013  constrinvcl  34014  constrresqrtcl  34018  constrabscl  34019  2sqr3minply  34021  cos9thpiminplylem1  34023  cos9thpiminply  34029  cos9thpinconstrlem1  34030  esumpfinvallem  34315  signsplypnf  34791  fsum2dsub  34848  logdivsqrle  34891  revpfxsfxrev  35404  cvxpconn  35530  cvxsconn  35531  fwddifnp1  36453  tan2h  38049  poimirlem16  38073  mbfposadd  38104  itg2addnc  38111  ftc1anclem5  38134  bfplem2  38260  aks4d1p1p4  42626  aks4d1p7d1  42637  primrootspoweq0  42661  aks6d1c1  42671  aks6d1c5lem1  42691  sticksstones10  42710  sticksstones22  42723  bcle2d  42734  dffltz  43154  3cubeslem3r  43206  pellexlem6  43349  jm2.18  43503  sqrtcval  44155  relexpaddss  44232  int-add02d  44699  sub2times  45790  fzisoeu  45817  xralrple2  45868  cosknegpi  46381  dvsinax  46425  dvasinbx  46432  dvnxpaek  46454  dvnmul  46455  stoweidlem1  46513  stoweidlem13  46525  stoweidlem42  46554  stirlinglem5  46590  stirlinglem11  46596  fourierdlem42  46661  fourierdlem51  46669  fourierdlem88  46706  fourierdlem103  46721  fourierdlem104  46722  fourierdlem107  46725  sqwvfoura  46740  sqwvfourb  46741  fouriersw  46743  elaa2lem  46745  hspmbllem1  47138  cnambpcma  47826  readdcnnred  47835  gpg3kgrtriex  48649  nn0mnd  48739  altgsumbcALT  48913  nn0sumshdiglemA  49179  line2xlem  49313  line2x  49314  itschlc0yqe  49320  itsclc0yqsollem1  49322  itschlc0xyqsol1  49326  itschlc0xyqsol  49327  2itscp  49341