Theorem addid1d 11105

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

Hypothesis

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

Assertion

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

Proof of Theorem addid1d

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

Syntax hints:   → wi 4   = wceq 1539   ∈ wcel 2108  (class class class)co 7255  ℂcc 10800  0cc0 10802   + caddc 10805

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-10 2139  ax-11 2156  ax-12 2173  ax-ext 2709  ax-sep 5218  ax-nul 5225  ax-pow 5283  ax-pr 5347  ax-un 7566  ax-resscn 10859  ax-1cn 10860  ax-icn 10861  ax-addcl 10862  ax-addrcl 10863  ax-mulcl 10864  ax-mulrcl 10865  ax-mulcom 10866  ax-addass 10867  ax-mulass 10868  ax-distr 10869  ax-i2m1 10870  ax-1ne0 10871  ax-1rid 10872  ax-rnegex 10873  ax-rrecex 10874  ax-cnre 10875  ax-pre-lttri 10876  ax-pre-lttrn 10877  ax-pre-ltadd 10878

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-3or 1086  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1784  df-nf 1788  df-sb 2069  df-mo 2540  df-eu 2569  df-clab 2716  df-cleq 2730  df-clel 2817  df-nfc 2888  df-ne 2943  df-nel 3049  df-ral 3068  df-rex 3069  df-rab 3072  df-v 3424  df-sbc 3712  df-csb 3829  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-nul 4254  df-if 4457  df-pw 4532  df-sn 4559  df-pr 4561  df-op 4565  df-uni 4837  df-br 5071  df-opab 5133  df-mpt 5154  df-id 5480  df-po 5494  df-so 5495  df-xp 5586  df-rel 5587  df-cnv 5588  df-co 5589  df-dm 5590  df-rn 5591  df-res 5592  df-ima 5593  df-iota 6376  df-fun 6420  df-fn 6421  df-f 6422  df-f1 6423  df-fo 6424  df-f1o 6425  df-fv 6426  df-ov 7258  df-er 8456  df-en 8692  df-dom 8693  df-sdom 8694  df-pnf 10942  df-mnf 10943  df-ltxr 10945

This theorem is referenced by:  ltaddneg  11120  subsub2  11179  negsub  11199  ltaddpos  11395  addge01  11415  add20  11417  nnge1  11931  nnnn0addcl  12193  un0addcl  12196  uzaddcl  12573  xaddid1  12904  fzosubel3  13376  expadd  13753  faclbnd4lem4  13938  faclbnd6  13941  hashgadd  14020  ccatrid  14220  pfxmpt  14319  pfxfv  14323  pfxswrd  14347  pfxccatin12lem1  14369  pfxccatin12lem2  14372  swrdccat3blem  14380  cshweqrep  14462  relexpaddg  14692  reim0b  14758  rereb  14759  immul2  14776  max0add  14950  iseraltlem2  15322  fsumsplit  15381  sumsplit  15408  binomfallfaclem2  15678  pwp1fsum  16028  bitsinv1lem  16076  sadadd2lem2  16085  sadcaddlem  16092  bezoutlem1  16175  pcadd  16518  pcadd2  16519  pcmpt  16521  vdwapun  16603  vdwlem1  16610  mulgnn0dir  18648  psgnunilem2  19018  sylow1lem1  19118  efginvrel2  19248  efgredleme  19264  efgcpbllemb  19276  frgpnabllem1  19389  regsumfsum  20578  regsumsupp  20739  mplcoe5  21151  xrsxmet  23878  reparphti  24066  cphpyth  24285  minveclem6  24503  ovolunnul  24569  voliunlem3  24621  ovolioo  24637  itg2splitlem  24818  itg2split  24819  itgrevallem1  24864  itgsplitioo  24907  ditgsplit  24930  dvnadd  24998  dvlipcn  25063  ply1divex  25206  dvntaylp  25435  ulmshft  25454  abelthlem6  25500  cosmpi  25550  sinppi  25551  sinhalfpip  25554  logrnaddcl  25635  affineequiv  25878  chordthmlem3  25889  atanlogaddlem  25968  atanlogsublem  25970  leibpi  25997  scvxcvx  26040  dmgmn0  26080  lgamgulmlem2  26084  lgambdd  26091  logexprlim  26278  2sqblem  26484  2sq2  26486  2sqnn  26492  dchrvmasum2if  26550  dchrvmasumlem  26576  axcontlem8  27242  elntg2  27256  crctcshlem4  28086  eupth2lem3lem6  28498  ipidsq  28973  minvecolem6  29145  normpyc  29409  pjspansn  29840  lnfnmuli  30307  hstoh  30495  archirngz  31345  indsumin  31890  esumpfinvallem  31942  signsvtp  32462  signlem0  32466  fsum2dsub  32487  cvxpconn  33104  cvxsconn  33105  elmrsubrn  33382  faclim2  33620  fwddifn0  34393  fwddifnp1  34394  dnizeq0  34582  knoppndvlem6  34624  bj-bary1lem  35408  poimirlem1  35705  poimirlem5  35709  poimirlem6  35710  poimirlem7  35711  poimirlem11  35715  poimirlem12  35716  poimirlem17  35721  poimirlem20  35724  poimirlem22  35726  poimirlem24  35728  poimirlem25  35729  poimirlem29  35733  poimirlem31  35735  mblfinlem2  35742  mbfposadd  35751  itg2addnc  35758  itgaddnclem2  35763  ftc1anclem5  35781  ftc1anclem8  35784  areacirc  35797  lcmineqlem4  39968  lcmineqlem18  39982  aks4d1p1p7  40010  aks4d1p3  40014  sticksstones10  40039  sticksstones12a  40041  metakunt29  40081  metakunt30  40082  3cubeslem2  40423  3cubeslem3r  40425  pell1qrgaplem  40611  jm2.19lem3  40729  jm2.25  40737  relexpaddss  41215  int-add01d  41684  binomcxplemnn0  41856  fperiodmullem  42732  xralrple3  42803  sumnnodd  43061  fprodaddrecnncnvlem  43340  ioodvbdlimc1lem2  43363  volioc  43403  volico  43414  stoweidlem11  43442  stoweidlem26  43457  stirlinglem12  43516  fourierdlem4  43542  fourierdlem42  43580  fourierdlem60  43597  fourierdlem61  43598  fourierdlem92  43629  fourierdlem107  43644  fouriersw  43662  etransclem24  43689  etransclem35  43700  hoidmvlelem2  44024  hspmbllem1  44054  sharhght  44268  deccarry  44691  nn0mnd  45261  altgsumbcALT  45577  itcovalpclem1  45904  eenglngeehlnmlem2  45972  line2y  45989  itschlc0xyqsol1  46000  itschlc0xyqsol  46001  2itscp  46015