Theorem addlidd 11491

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

Syntax hints:   → wi 4   = wceq 1537   ∈ wcel 2108  (class class class)co 7448  ℂcc 11182  0cc0 11184   + caddc 11187

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2158  ax-12 2178  ax-ext 2711  ax-sep 5317  ax-nul 5324  ax-pow 5383  ax-pr 5447  ax-un 7770  ax-resscn 11241  ax-1cn 11242  ax-icn 11243  ax-addcl 11244  ax-addrcl 11245  ax-mulcl 11246  ax-mulrcl 11247  ax-mulcom 11248  ax-addass 11249  ax-mulass 11250  ax-distr 11251  ax-i2m1 11252  ax-1ne0 11253  ax-1rid 11254  ax-rnegex 11255  ax-rrecex 11256  ax-cnre 11257  ax-pre-lttri 11258  ax-pre-lttrn 11259  ax-pre-ltadd 11260

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 847  df-3or 1088  df-3an 1089  df-tru 1540  df-fal 1550  df-ex 1778  df-nf 1782  df-sb 2065  df-mo 2543  df-eu 2572  df-clab 2718  df-cleq 2732  df-clel 2819  df-nfc 2895  df-ne 2947  df-nel 3053  df-ral 3068  df-rex 3077  df-rab 3444  df-v 3490  df-sbc 3805  df-csb 3922  df-dif 3979  df-un 3981  df-in 3983  df-ss 3993  df-nul 4353  df-if 4549  df-pw 4624  df-sn 4649  df-pr 4651  df-op 4655  df-uni 4932  df-br 5167  df-opab 5229  df-mpt 5250  df-id 5593  df-po 5607  df-so 5608  df-xp 5706  df-rel 5707  df-cnv 5708  df-co 5709  df-dm 5710  df-rn 5711  df-res 5712  df-ima 5713  df-iota 6525  df-fun 6575  df-fn 6576  df-f 6577  df-f1 6578  df-fo 6579  df-f1o 6580  df-fv 6581  df-ov 7451  df-er 8763  df-en 9004  df-dom 9005  df-sdom 9006  df-pnf 11326  df-mnf 11327  df-ltxr 11329

This theorem is referenced by:  negeu  11526  subge0  11803  sublt0d  11916  un0addcl  12586  lincmb01cmp  13555  ico01fl0  13870  discr  14289  ccatlid  14634  swrdfv0  14697  swrdpfx  14755  pfxpfx  14756  cats1un  14769  swrdccatin2  14777  cshwidx0mod  14853  cshw1  14870  relexpaddg  15102  rennim  15288  max0add  15359  fsumsplit  15789  sumsplit  15816  isumsplit  15888  arisum2  15909  binomfallfaclem2  16088  efaddlem  16141  eftlub  16157  ef4p  16161  rpnnen2lem11  16272  moddvds  16313  divalglem9  16449  sadadd2lem2  16496  sadcaddlem  16503  gcdmultipled  16581  pcmpt  16939  4sqlem11  17002  vdwlem6  17033  gsumsgrpccat  18875  mulgnn0dir  19144  sylow1lem1  19640  efgsval2  19775  efgsp1  19779  zaddablx  19914  pgpfaclem1  20125  regsumfsum  21476  regsumsupp  21663  mplcoe5  22081  nrmmetd  24608  blcvx  24839  xrsxmet  24850  reparphti  25048  reparphtiOLD  25049  nulmbl  25589  itg2splitlem  25803  itg2split  25804  itg2monolem1  25805  itgsplitioo  25893  ditgsplit  25916  dvcnp2  25975  dvcnp2OLD  25976  dvcmul  26001  dvcmulf  26002  dvmptcmul  26022  dveflem  26037  dvef  26038  dvlipcn  26053  dvlt0  26064  plymullem1  26273  coeeulem  26283  dgradd2  26328  dgrmulc  26331  plydivlem3  26355  aareccl  26386  taylthlem1  26433  sin2kpi  26543  cos2kpi  26544  coshalfpim  26555  sinkpi  26582  chordthmlem3  26895  chordthmlem5  26897  dcubic1lem  26904  dcubic  26907  atancj  26971  atanlogaddlem  26974  atanlogsublem  26976  scvxcvx  27047  zetacvg  27076  ftalem5  27138  ftalem7  27140  basellem3  27144  chtublem  27273  2sqn0  27496  2sqnn  27501  rplogsumlem2  27547  dchrisumlem1  27551  pntrlog2bndlem2  27640  brbtwn2  28938  axlowdimlem16  28990  axeuclidlem  28995  elntg2  29018  eucrct2eupth  30277  2clwwlk2clwwlk  30382  re0cj  32756  bcm1n  32800  wrdt2ind  32920  2sqr3minply  33738  esumpfinvallem  34038  signsplypnf  34527  fsum2dsub  34584  logdivsqrle  34627  revpfxsfxrev  35083  cvxpconn  35210  cvxsconn  35211  fwddifnp1  36129  tan2h  37572  poimirlem16  37596  mbfposadd  37627  itg2addnc  37634  ftc1anclem5  37657  bfplem2  37783  aks4d1p1p4  42028  aks4d1p7d1  42039  primrootspoweq0  42063  aks6d1c1  42073  aks6d1c5lem1  42093  sticksstones10  42112  sticksstones22  42125  bcle2d  42136  dffltz  42589  3cubeslem3r  42643  pellexlem6  42790  jm2.18  42945  sqrtcval  43603  relexpaddss  43680  int-add02d  44147  sub2times  45187  fzisoeu  45215  xralrple2  45269  cosknegpi  45790  dvsinax  45834  dvasinbx  45841  dvnxpaek  45863  dvnmul  45864  stoweidlem1  45922  stoweidlem13  45934  stoweidlem42  45963  stirlinglem5  45999  stirlinglem11  46005  fourierdlem42  46070  fourierdlem51  46078  fourierdlem88  46115  fourierdlem103  46130  fourierdlem104  46131  fourierdlem107  46134  sqwvfoura  46149  sqwvfourb  46150  fouriersw  46152  elaa2lem  46154  hspmbllem1  46547  cnambpcma  47209  readdcnnred  47218  nn0mnd  47902  altgsumbcALT  48078  nn0sumshdiglemA  48353  line2xlem  48487  line2x  48488  itschlc0yqe  48494  itsclc0yqsollem1  48496  itschlc0xyqsol1  48500  itschlc0xyqsol  48501  2itscp  48515