Theorem addridd 11381

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

Syntax hints:   → wi 4   = wceq 1540   ∈ wcel 2109  (class class class)co 7390  ℂcc 11073  0cc0 11075   + caddc 11078

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2702  ax-sep 5254  ax-nul 5264  ax-pow 5323  ax-pr 5390  ax-un 7714  ax-resscn 11132  ax-1cn 11133  ax-icn 11134  ax-addcl 11135  ax-addrcl 11136  ax-mulcl 11137  ax-mulrcl 11138  ax-mulcom 11139  ax-addass 11140  ax-mulass 11141  ax-distr 11142  ax-i2m1 11143  ax-1ne0 11144  ax-1rid 11145  ax-rnegex 11146  ax-rrecex 11147  ax-cnre 11148  ax-pre-lttri 11149  ax-pre-lttrn 11150  ax-pre-ltadd 11151

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2534  df-eu 2563  df-clab 2709  df-cleq 2722  df-clel 2804  df-nfc 2879  df-ne 2927  df-nel 3031  df-ral 3046  df-rex 3055  df-rab 3409  df-v 3452  df-sbc 3757  df-csb 3866  df-dif 3920  df-un 3922  df-in 3924  df-ss 3934  df-nul 4300  df-if 4492  df-pw 4568  df-sn 4593  df-pr 4595  df-op 4599  df-uni 4875  df-br 5111  df-opab 5173  df-mpt 5192  df-id 5536  df-po 5549  df-so 5550  df-xp 5647  df-rel 5648  df-cnv 5649  df-co 5650  df-dm 5651  df-rn 5652  df-res 5653  df-ima 5654  df-iota 6467  df-fun 6516  df-fn 6517  df-f 6518  df-f1 6519  df-fo 6520  df-f1o 6521  df-fv 6522  df-ov 7393  df-er 8674  df-en 8922  df-dom 8923  df-sdom 8924  df-pnf 11217  df-mnf 11218  df-ltxr 11220

This theorem is referenced by:  ltaddneg  11397  subsub2  11457  negsub  11477  ltaddpos  11675  addge01  11695  add20  11697  nnge1  12221  nnnn0addcl  12479  un0addcl  12482  uzaddcl  12870  xaddrid  13208  fzosubel3  13694  expadd  14076  faclbnd4lem4  14268  faclbnd6  14271  hashgadd  14349  ccatrid  14559  pfxmpt  14650  pfxfv  14654  pfxswrd  14678  pfxccatin12lem1  14700  pfxccatin12lem2  14703  swrdccat3blem  14711  cshweqrep  14793  relexpaddg  15026  reim0b  15092  rereb  15093  immul2  15110  max0add  15283  iseraltlem2  15656  fsumsplit  15714  sumsplit  15741  binomfallfaclem2  16013  pwp1fsum  16368  bitsinv1lem  16418  sadadd2lem2  16427  sadcaddlem  16434  bezoutlem1  16516  pcadd  16867  pcadd2  16868  pcmpt  16870  vdwapun  16952  vdwlem1  16959  mulgnn0dir  19043  psgnunilem2  19432  sylow1lem1  19535  efginvrel2  19664  efgredleme  19680  efgcpbllemb  19692  frgpnabllem1  19810  regsumfsum  21359  pzriprnglem10  21407  regsumsupp  21538  mplcoe5  21954  psdmul  22060  xrsxmet  24705  reparphti  24903  reparphtiOLD  24904  cphpyth  25123  minveclem6  25341  ovolunnul  25408  voliunlem3  25460  ovolioo  25476  itg2splitlem  25656  itg2split  25657  itgrevallem1  25703  itgsplitioo  25746  ditgsplit  25769  dvnadd  25838  dvlipcn  25906  ply1divex  26049  dvntaylp  26286  ulmshft  26306  abelthlem6  26353  cosmpi  26404  sinppi  26405  sinhalfpip  26408  logrnaddcl  26490  affineequiv  26740  chordthmlem3  26751  atanlogaddlem  26830  atanlogsublem  26832  leibpi  26859  scvxcvx  26903  dmgmn0  26943  lgamgulmlem2  26947  lgambdd  26954  logexprlim  27143  2sqblem  27349  2sq2  27351  2sqnn  27357  dchrvmasum2if  27415  dchrvmasumlem  27441  axcontlem8  28905  elntg2  28919  crctcshlem4  29757  eupth2lem3lem6  30169  ipidsq  30646  minvecolem6  30818  normpyc  31082  pjspansn  31513  lnfnmuli  31980  hstoh  32168  indsumin  32792  archirngz  33150  constrrtlc2  33730  constrsslem  33738  2sqr3minply  33777  cos9thpiminply  33785  esumpfinvallem  34071  signsvtp  34581  signlem0  34585  fsum2dsub  34605  cvxpconn  35236  cvxsconn  35237  elmrsubrn  35514  faclim2  35742  fwddifn0  36159  fwddifnp1  36160  dnizeq0  36470  knoppndvlem6  36512  bj-bary1lem  37305  poimirlem1  37622  poimirlem5  37626  poimirlem6  37627  poimirlem7  37628  poimirlem11  37632  poimirlem12  37633  poimirlem17  37638  poimirlem20  37641  poimirlem22  37643  poimirlem24  37645  poimirlem25  37646  poimirlem29  37650  poimirlem31  37652  mblfinlem2  37659  mbfposadd  37668  itg2addnc  37675  itgaddnclem2  37680  ftc1anclem5  37698  ftc1anclem8  37701  areacirc  37714  lcmineqlem4  42027  lcmineqlem18  42041  aks4d1p1p7  42069  aks4d1p3  42073  posbezout  42095  primrootspoweq0  42101  sticksstones10  42150  sticksstones12a  42152  unitscyglem5  42194  3cubeslem2  42680  3cubeslem3r  42682  pell1qrgaplem  42868  jm2.19lem3  42987  jm2.25  42995  relexpaddss  43714  int-add01d  44180  binomcxplemnn0  44345  fperiodmullem  45308  xralrple3  45377  sumnnodd  45635  fprodaddrecnncnvlem  45914  ioodvbdlimc1lem2  45937  volioc  45977  volico  45988  stoweidlem11  46016  stoweidlem26  46031  stirlinglem12  46090  fourierdlem4  46116  fourierdlem42  46154  fourierdlem60  46171  fourierdlem61  46172  fourierdlem92  46203  fourierdlem107  46218  fouriersw  46236  etransclem24  46263  etransclem35  46274  hoidmvlelem2  46601  hspmbllem1  46631  sharhght  46870  deccarry  47316  nn0mnd  48171  altgsumbcALT  48345  itcovalpclem1  48663  eenglngeehlnmlem2  48731  line2y  48748  itschlc0xyqsol1  48759  itschlc0xyqsol  48760  2itscp  48774