Theorem addid1d 11184

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

Syntax hints:   → wi 4   = wceq 1539   ∈ wcel 2107  (class class class)co 7284  ℂcc 10878  0cc0 10880   + caddc 10883

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2710  ax-sep 5224  ax-nul 5231  ax-pow 5289  ax-pr 5353  ax-un 7597  ax-resscn 10937  ax-1cn 10938  ax-icn 10939  ax-addcl 10940  ax-addrcl 10941  ax-mulcl 10942  ax-mulrcl 10943  ax-mulcom 10944  ax-addass 10945  ax-mulass 10946  ax-distr 10947  ax-i2m1 10948  ax-1ne0 10949  ax-1rid 10950  ax-rnegex 10951  ax-rrecex 10952  ax-cnre 10953  ax-pre-lttri 10954  ax-pre-lttrn 10955  ax-pre-ltadd 10956

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3or 1087  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2541  df-eu 2570  df-clab 2717  df-cleq 2731  df-clel 2817  df-nfc 2890  df-ne 2945  df-nel 3051  df-ral 3070  df-rex 3071  df-rab 3074  df-v 3435  df-sbc 3718  df-csb 3834  df-dif 3891  df-un 3893  df-in 3895  df-ss 3905  df-nul 4258  df-if 4461  df-pw 4536  df-sn 4563  df-pr 4565  df-op 4569  df-uni 4841  df-br 5076  df-opab 5138  df-mpt 5159  df-id 5490  df-po 5504  df-so 5505  df-xp 5596  df-rel 5597  df-cnv 5598  df-co 5599  df-dm 5600  df-rn 5601  df-res 5602  df-ima 5603  df-iota 6395  df-fun 6439  df-fn 6440  df-f 6441  df-f1 6442  df-fo 6443  df-f1o 6444  df-fv 6445  df-ov 7287  df-er 8507  df-en 8743  df-dom 8744  df-sdom 8745  df-pnf 11020  df-mnf 11021  df-ltxr 11023

This theorem is referenced by:  ltaddneg  11199  subsub2  11258  negsub  11278  ltaddpos  11474  addge01  11494  add20  11496  nnge1  12010  nnnn0addcl  12272  un0addcl  12275  uzaddcl  12653  xaddid1  12984  fzosubel3  13457  expadd  13834  faclbnd4lem4  14019  faclbnd6  14022  hashgadd  14101  ccatrid  14301  pfxmpt  14400  pfxfv  14404  pfxswrd  14428  pfxccatin12lem1  14450  pfxccatin12lem2  14453  swrdccat3blem  14461  cshweqrep  14543  relexpaddg  14773  reim0b  14839  rereb  14840  immul2  14857  max0add  15031  iseraltlem2  15403  fsumsplit  15462  sumsplit  15489  binomfallfaclem2  15759  pwp1fsum  16109  bitsinv1lem  16157  sadadd2lem2  16166  sadcaddlem  16173  bezoutlem1  16256  pcadd  16599  pcadd2  16600  pcmpt  16602  vdwapun  16684  vdwlem1  16691  mulgnn0dir  18742  psgnunilem2  19112  sylow1lem1  19212  efginvrel2  19342  efgredleme  19358  efgcpbllemb  19370  frgpnabllem1  19483  regsumfsum  20675  regsumsupp  20836  mplcoe5  21250  xrsxmet  23981  reparphti  24169  cphpyth  24389  minveclem6  24607  ovolunnul  24673  voliunlem3  24725  ovolioo  24741  itg2splitlem  24922  itg2split  24923  itgrevallem1  24968  itgsplitioo  25011  ditgsplit  25034  dvnadd  25102  dvlipcn  25167  ply1divex  25310  dvntaylp  25539  ulmshft  25558  abelthlem6  25604  cosmpi  25654  sinppi  25655  sinhalfpip  25658  logrnaddcl  25739  affineequiv  25982  chordthmlem3  25993  atanlogaddlem  26072  atanlogsublem  26074  leibpi  26101  scvxcvx  26144  dmgmn0  26184  lgamgulmlem2  26188  lgambdd  26195  logexprlim  26382  2sqblem  26588  2sq2  26590  2sqnn  26596  dchrvmasum2if  26654  dchrvmasumlem  26680  axcontlem8  27348  elntg2  27362  crctcshlem4  28194  eupth2lem3lem6  28606  ipidsq  29081  minvecolem6  29253  normpyc  29517  pjspansn  29948  lnfnmuli  30415  hstoh  30603  archirngz  31452  indsumin  31999  esumpfinvallem  32051  signsvtp  32571  signlem0  32575  fsum2dsub  32596  cvxpconn  33213  cvxsconn  33214  elmrsubrn  33491  faclim2  33723  fwddifn0  34475  fwddifnp1  34476  dnizeq0  34664  knoppndvlem6  34706  bj-bary1lem  35490  poimirlem1  35787  poimirlem5  35791  poimirlem6  35792  poimirlem7  35793  poimirlem11  35797  poimirlem12  35798  poimirlem17  35803  poimirlem20  35806  poimirlem22  35808  poimirlem24  35810  poimirlem25  35811  poimirlem29  35815  poimirlem31  35817  mblfinlem2  35824  mbfposadd  35833  itg2addnc  35840  itgaddnclem2  35845  ftc1anclem5  35863  ftc1anclem8  35866  areacirc  35879  lcmineqlem4  40047  lcmineqlem18  40061  aks4d1p1p7  40089  aks4d1p3  40093  sticksstones10  40118  sticksstones12a  40120  metakunt29  40160  metakunt30  40161  3cubeslem2  40514  3cubeslem3r  40516  pell1qrgaplem  40702  jm2.19lem3  40820  jm2.25  40828  relexpaddss  41333  int-add01d  41802  binomcxplemnn0  41974  fperiodmullem  42849  xralrple3  42920  sumnnodd  43178  fprodaddrecnncnvlem  43457  ioodvbdlimc1lem2  43480  volioc  43520  volico  43531  stoweidlem11  43559  stoweidlem26  43574  stirlinglem12  43633  fourierdlem4  43659  fourierdlem42  43697  fourierdlem60  43714  fourierdlem61  43715  fourierdlem92  43746  fourierdlem107  43761  fouriersw  43779  etransclem24  43806  etransclem35  43817  hoidmvlelem2  44141  hspmbllem1  44171  sharhght  44392  deccarry  44814  nn0mnd  45384  altgsumbcALT  45700  itcovalpclem1  46027  eenglngeehlnmlem2  46095  line2y  46112  itschlc0xyqsol1  46123  itschlc0xyqsol  46124  2itscp  46138