Theorem addid2d 10577

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

Syntax hints:   → wi 4   = wceq 1601   ∈ wcel 2107  (class class class)co 6922  ℂcc 10270  0cc0 10272   + caddc 10275

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1839  ax-4 1853  ax-5 1953  ax-6 2021  ax-7 2055  ax-8 2109  ax-9 2116  ax-10 2135  ax-11 2150  ax-12 2163  ax-13 2334  ax-ext 2754  ax-sep 5017  ax-nul 5025  ax-pow 5077  ax-pr 5138  ax-un 7226  ax-resscn 10329  ax-1cn 10330  ax-icn 10331  ax-addcl 10332  ax-addrcl 10333  ax-mulcl 10334  ax-mulrcl 10335  ax-mulcom 10336  ax-addass 10337  ax-mulass 10338  ax-distr 10339  ax-i2m1 10340  ax-1ne0 10341  ax-1rid 10342  ax-rnegex 10343  ax-rrecex 10344  ax-cnre 10345  ax-pre-lttri 10346  ax-pre-lttrn 10347  ax-pre-ltadd 10348

This theorem depends on definitions:  df-bi 199  df-an 387  df-or 837  df-3or 1072  df-3an 1073  df-tru 1605  df-ex 1824  df-nf 1828  df-sb 2012  df-mo 2551  df-eu 2587  df-clab 2764  df-cleq 2770  df-clel 2774  df-nfc 2921  df-ne 2970  df-nel 3076  df-ral 3095  df-rex 3096  df-rab 3099  df-v 3400  df-sbc 3653  df-csb 3752  df-dif 3795  df-un 3797  df-in 3799  df-ss 3806  df-nul 4142  df-if 4308  df-pw 4381  df-sn 4399  df-pr 4401  df-op 4405  df-uni 4672  df-br 4887  df-opab 4949  df-mpt 4966  df-id 5261  df-po 5274  df-so 5275  df-xp 5361  df-rel 5362  df-cnv 5363  df-co 5364  df-dm 5365  df-rn 5366  df-res 5367  df-ima 5368  df-iota 6099  df-fun 6137  df-fn 6138  df-f 6139  df-f1 6140  df-fo 6141  df-f1o 6142  df-fv 6143  df-ov 6925  df-er 8026  df-en 8242  df-dom 8243  df-sdom 8244  df-pnf 10413  df-mnf 10414  df-ltxr 10416

This theorem is referenced by:  negeu  10612  subge0  10888  sublt0d  11001  un0addcl  11677  lincmb01cmp  12632  ico01fl0  12939  discr  13320  ccatlid  13676  swrdfv0  13741  swrdswrd0OLD  13817  swrdpfx  13818  pfxpfx  13820  cats1un  13841  swrdccatin2  13856  cshwidx0mod  13956  cshw1  13973  relexpaddg  14200  rennim  14386  max0add  14457  fsumsplit  14878  sumsplit  14904  isumsplit  14976  arisum2  14997  binomfallfaclem2  15173  efaddlem  15225  eftlub  15241  ef4p  15245  rpnnen2lem11  15357  moddvds  15398  divalglem9  15531  sadadd2lem2  15578  sadcaddlem  15585  pcmpt  16000  4sqlem11  16063  vdwlem6  16094  gsumccat  17764  mulgnn0dir  17956  sylow1lem1  18397  efgsval2  18530  efgsp1  18534  zaddablx  18661  pgpfaclem1  18867  mplcoe5  19865  regsumfsum  20210  regsumsupp  20365  nrmmetd  22787  blcvx  23009  xrsxmet  23020  reparphti  23204  nulmbl  23739  itg2splitlem  23952  itg2split  23953  itg2monolem1  23954  itgsplitioo  24041  ditgsplit  24062  dvcnp2  24120  dvcmul  24144  dvcmulf  24145  dvmptcmul  24164  dveflem  24179  dvef  24180  dvlipcn  24194  dvlt0  24205  plymullem1  24407  coeeulem  24417  dgradd2  24461  dgrmulc  24464  plydivlem3  24487  aareccl  24518  taylthlem1  24564  sin2kpi  24673  cos2kpi  24674  coshalfpim  24685  sinkpi  24709  chordthmlem3  25012  chordthmlem5  25014  dcubic1lem  25021  dcubic  25024  atancj  25088  atanlogaddlem  25091  atanlogsublem  25093  scvxcvx  25164  zetacvg  25193  ftalem5  25255  ftalem7  25257  basellem3  25261  chtublem  25388  rplogsumlem2  25626  dchrisumlem1  25630  pntrlog2bndlem2  25719  brbtwn2  26254  axlowdimlem16  26306  axeuclidlem  26311  elntg2  26334  eucrct2eupthOLD  27650  eucrct2eupth  27651  2clwwlk2clwwlk  27761  2clwwlk2clwwlkOLD  27762  bcm1n  30118  2sqn0  30208  esumpfinvallem  30734  signsplypnf  31227  signstfvn  31246  fsum2dsub  31287  logdivsqrle  31330  cvxpconn  31823  cvxsconn  31824  fwddifnp1  32861  tan2h  34028  poimirlem16  34053  mbfposadd  34084  itg2addnc  34091  ftc1anclem5  34116  bfplem2  34248  dffltz  38217  pellexlem6  38362  jm2.18  38518  relexpaddss  38971  int-add02d  39448  sub2times  40400  fzisoeu  40427  xralrple2  40482  cosknegpi  41012  dvsinax  41059  dvasinbx  41067  dvnxpaek  41089  dvnmul  41090  stoweidlem1  41149  stoweidlem13  41161  stoweidlem42  41190  stirlinglem5  41226  stirlinglem11  41232  fourierdlem42  41297  fourierdlem51  41305  fourierdlem88  41342  fourierdlem103  41357  fourierdlem104  41358  fourierdlem107  41361  sqwvfoura  41376  sqwvfourb  41377  fouriersw  41379  elaa2lem  41381  hspmbllem1  41771  cnambpcma  42340  readdcnnred  42349  altgsumbcALT  43150  nn0sumshdiglemA  43432  line2xlem  43493  line2x  43494  itschlc0yqe  43500  itsclc0yqsollem1  43502  itschlc0xyqsol1  43506  itschlc0xyqsol  43507  2itscp  43521