Theorem addridd 11335

Description: 0 is an additive identity. (Contributed by Mario Carneiro, 27-May-2016.)

Hypothesis

Ref	Expression
muld.1	⊢ (𝜑 → 𝐴 ∈ ℂ)

Assertion

Ref	Expression
addridd	⊢ (𝜑 → (𝐴 + 0) = 𝐴)

Proof of Theorem addridd

Step	Hyp	Ref	Expression
1		muld.1	. 2 ⊢ (𝜑 → 𝐴 ∈ ℂ)
2		addrid 11315	. 2 ⊢ (𝐴 ∈ ℂ → (𝐴 + 0) = 𝐴)
3	1, 2	syl 17	1 ⊢ (𝜑 → (𝐴 + 0) = 𝐴)

Syntax hints:   → wi 4   = wceq 1542   ∈ wcel 2114  (class class class)co 7356  ℂcc 11025  0cc0 11027   + caddc 11030

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2184  ax-ext 2707  ax-sep 5220  ax-nul 5230  ax-pow 5296  ax-pr 5364  ax-un 7678  ax-resscn 11084  ax-1cn 11085  ax-icn 11086  ax-addcl 11087  ax-addrcl 11088  ax-mulcl 11089  ax-mulrcl 11090  ax-mulcom 11091  ax-addass 11092  ax-mulass 11093  ax-distr 11094  ax-i2m1 11095  ax-1ne0 11096  ax-1rid 11097  ax-rnegex 11098  ax-rrecex 11099  ax-cnre 11100  ax-pre-lttri 11101  ax-pre-lttrn 11102  ax-pre-ltadd 11103

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2538  df-eu 2568  df-clab 2714  df-cleq 2727  df-clel 2810  df-nfc 2884  df-ne 2931  df-nel 3035  df-ral 3050  df-rex 3060  df-rab 3388  df-v 3429  df-sbc 3726  df-csb 3834  df-dif 3888  df-un 3890  df-in 3892  df-ss 3902  df-nul 4264  df-if 4457  df-pw 4533  df-sn 4558  df-pr 4560  df-op 4564  df-uni 4841  df-br 5075  df-opab 5137  df-mpt 5156  df-id 5515  df-po 5528  df-so 5529  df-xp 5626  df-rel 5627  df-cnv 5628  df-co 5629  df-dm 5630  df-rn 5631  df-res 5632  df-ima 5633  df-iota 6443  df-fun 6489  df-fn 6490  df-f 6491  df-f1 6492  df-fo 6493  df-f1o 6494  df-fv 6495  df-ov 7359  df-er 8632  df-en 8883  df-dom 8884  df-sdom 8885  df-pnf 11170  df-mnf 11171  df-ltxr 11173

This theorem is referenced by:  ltaddneg  11351  subsub2  11411  negsub  11431  ltaddpos  11629  addge01  11649  add20  11651  nnge1  12194  nnnn0addcl  12456  un0addcl  12459  uzaddcl  12843  xaddrid  13182  fzosubel3  13670  expadd  14055  faclbnd4lem4  14247  faclbnd6  14250  hashgadd  14328  ccatrid  14539  pfxmpt  14630  pfxfv  14634  pfxswrd  14657  pfxccatin12lem1  14679  pfxccatin12lem2  14682  swrdccat3blem  14690  cshweqrep  14772  relexpaddg  15004  reim0b  15070  rereb  15071  immul2  15088  max0add  15261  iseraltlem2  15634  fsumsplit  15692  sumsplit  15719  binomfallfaclem2  15994  pwp1fsum  16349  bitsinv1lem  16399  sadadd2lem2  16408  sadcaddlem  16415  bezoutlem1  16497  pcadd  16849  pcadd2  16850  pcmpt  16852  vdwapun  16934  vdwlem1  16941  chnccat  18581  mulgnn0dir  19069  psgnunilem2  19459  sylow1lem1  19562  efginvrel2  19691  efgredleme  19707  efgcpbllemb  19719  frgpnabllem1  19837  regsumfsum  21404  pzriprnglem10  21459  regsumsupp  21591  mplcoe5  22007  psdmul  22121  xrsxmet  24763  reparphti  24952  cphpyth  25171  minveclem6  25389  ovolunnul  25455  voliunlem3  25507  ovolioo  25523  itg2splitlem  25703  itg2split  25704  itgrevallem1  25750  itgsplitioo  25793  ditgsplit  25816  dvnadd  25884  dvlipcn  25949  ply1divex  26090  dvntaylp  26324  ulmshft  26343  abelthlem6  26389  cosmpi  26440  sinppi  26441  sinhalfpip  26444  logrnaddcl  26526  affineequiv  26775  chordthmlem3  26786  atanlogaddlem  26865  atanlogsublem  26867  leibpi  26894  scvxcvx  26937  dmgmn0  26977  lgamgulmlem2  26981  lgambdd  26988  logexprlim  27176  2sqblem  27382  2sq2  27384  2sqnn  27390  dchrvmasum2if  27448  dchrvmasumlem  27474  axcontlem8  29028  elntg2  29042  crctcshlem4  29876  eupth2lem3lem6  30291  ipidsq  30769  minvecolem6  30941  normpyc  31205  pjspansn  31636  lnfnmuli  32103  hstoh  32291  indsumin  32909  archirngz  33238  constrrtlc2  33865  constrsslem  33873  2sqr3minply  33912  cos9thpiminply  33920  esumpfinvallem  34206  signsvtp  34715  signlem0  34719  fsum2dsub  34739  cvxpconn  35412  cvxsconn  35413  elmrsubrn  35690  faclim2  35918  fwddifn0  36334  fwddifnp1  36335  dnizeq0  36723  knoppndvlem6  36765  bj-bary1lem  37612  poimirlem1  37930  poimirlem5  37934  poimirlem6  37935  poimirlem7  37936  poimirlem11  37940  poimirlem12  37941  poimirlem17  37946  poimirlem20  37949  poimirlem22  37951  poimirlem24  37953  poimirlem25  37954  poimirlem29  37958  poimirlem31  37960  mblfinlem2  37967  mbfposadd  37976  itg2addnc  37983  itgaddnclem2  37988  ftc1anclem5  38006  ftc1anclem8  38009  areacirc  38022  lcmineqlem4  42459  lcmineqlem18  42473  aks4d1p1p7  42501  aks4d1p3  42505  posbezout  42527  primrootspoweq0  42533  sticksstones10  42582  sticksstones12a  42584  unitscyglem5  42626  3cubeslem2  43105  3cubeslem3r  43107  pell1qrgaplem  43289  jm2.19lem3  43407  jm2.25  43415  relexpaddss  44133  int-add01d  44599  binomcxplemnn0  44764  fperiodmullem  45724  xralrple3  45791  sumnnodd  46048  fprodaddrecnncnvlem  46325  ioodvbdlimc1lem2  46348  volioc  46388  volico  46399  stoweidlem11  46427  stoweidlem26  46442  stirlinglem12  46501  fourierdlem4  46527  fourierdlem42  46565  fourierdlem60  46582  fourierdlem61  46583  fourierdlem92  46614  fourierdlem107  46629  fouriersw  46647  etransclem24  46674  etransclem35  46685  hoidmvlelem2  47012  hspmbllem1  47042  sharhght  47281  deccarry  47747  flmrecm1  47779  nn0mnd  48643  altgsumbcALT  48817  itcovalpclem1  49134  eenglngeehlnmlem2  49202  line2y  49219  itschlc0xyqsol1  49230  itschlc0xyqsol  49231  2itscp  49245