Theorem addridd 11413

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

Syntax hints:   → wi 4   = wceq 1541   ∈ wcel 2106  (class class class)co 7408  ℂcc 11107  0cc0 11109   + caddc 11112

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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2703  ax-sep 5299  ax-nul 5306  ax-pow 5363  ax-pr 5427  ax-un 7724  ax-resscn 11166  ax-1cn 11167  ax-icn 11168  ax-addcl 11169  ax-addrcl 11170  ax-mulcl 11171  ax-mulrcl 11172  ax-mulcom 11173  ax-addass 11174  ax-mulass 11175  ax-distr 11176  ax-i2m1 11177  ax-1ne0 11178  ax-1rid 11179  ax-rnegex 11180  ax-rrecex 11181  ax-cnre 11182  ax-pre-lttri 11183  ax-pre-lttrn 11184  ax-pre-ltadd 11185

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3or 1088  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2534  df-eu 2563  df-clab 2710  df-cleq 2724  df-clel 2810  df-nfc 2885  df-ne 2941  df-nel 3047  df-ral 3062  df-rex 3071  df-rab 3433  df-v 3476  df-sbc 3778  df-csb 3894  df-dif 3951  df-un 3953  df-in 3955  df-ss 3965  df-nul 4323  df-if 4529  df-pw 4604  df-sn 4629  df-pr 4631  df-op 4635  df-uni 4909  df-br 5149  df-opab 5211  df-mpt 5232  df-id 5574  df-po 5588  df-so 5589  df-xp 5682  df-rel 5683  df-cnv 5684  df-co 5685  df-dm 5686  df-rn 5687  df-res 5688  df-ima 5689  df-iota 6495  df-fun 6545  df-fn 6546  df-f 6547  df-f1 6548  df-fo 6549  df-f1o 6550  df-fv 6551  df-ov 7411  df-er 8702  df-en 8939  df-dom 8940  df-sdom 8941  df-pnf 11249  df-mnf 11250  df-ltxr 11252

This theorem is referenced by:  ltaddneg  11428  subsub2  11487  negsub  11507  ltaddpos  11703  addge01  11723  add20  11725  nnge1  12239  nnnn0addcl  12501  un0addcl  12504  uzaddcl  12887  xaddrid  13219  fzosubel3  13692  expadd  14069  faclbnd4lem4  14255  faclbnd6  14258  hashgadd  14336  ccatrid  14536  pfxmpt  14627  pfxfv  14631  pfxswrd  14655  pfxccatin12lem1  14677  pfxccatin12lem2  14680  swrdccat3blem  14688  cshweqrep  14770  relexpaddg  14999  reim0b  15065  rereb  15066  immul2  15083  max0add  15256  iseraltlem2  15628  fsumsplit  15686  sumsplit  15713  binomfallfaclem2  15983  pwp1fsum  16333  bitsinv1lem  16381  sadadd2lem2  16390  sadcaddlem  16397  bezoutlem1  16480  pcadd  16821  pcadd2  16822  pcmpt  16824  vdwapun  16906  vdwlem1  16913  mulgnn0dir  18983  psgnunilem2  19362  sylow1lem1  19465  efginvrel2  19594  efgredleme  19610  efgcpbllemb  19622  frgpnabllem1  19740  regsumfsum  21012  regsumsupp  21174  mplcoe5  21594  xrsxmet  24324  reparphti  24512  cphpyth  24732  minveclem6  24950  ovolunnul  25016  voliunlem3  25068  ovolioo  25084  itg2splitlem  25265  itg2split  25266  itgrevallem1  25311  itgsplitioo  25354  ditgsplit  25377  dvnadd  25445  dvlipcn  25510  ply1divex  25653  dvntaylp  25882  ulmshft  25901  abelthlem6  25947  cosmpi  25997  sinppi  25998  sinhalfpip  26001  logrnaddcl  26082  affineequiv  26325  chordthmlem3  26336  atanlogaddlem  26415  atanlogsublem  26417  leibpi  26444  scvxcvx  26487  dmgmn0  26527  lgamgulmlem2  26531  lgambdd  26538  logexprlim  26725  2sqblem  26931  2sq2  26933  2sqnn  26939  dchrvmasum2if  26997  dchrvmasumlem  27023  axcontlem8  28226  elntg2  28240  crctcshlem4  29071  eupth2lem3lem6  29483  ipidsq  29958  minvecolem6  30130  normpyc  30394  pjspansn  30825  lnfnmuli  31292  hstoh  31480  archirngz  32330  indsumin  33015  esumpfinvallem  33067  signsvtp  33589  signlem0  33593  fsum2dsub  33614  cvxpconn  34228  cvxsconn  34229  elmrsubrn  34506  faclim2  34713  fwddifn0  35131  fwddifnp1  35132  gg-reparphti  35167  dnizeq0  35346  knoppndvlem6  35388  bj-bary1lem  36186  poimirlem1  36484  poimirlem5  36488  poimirlem6  36489  poimirlem7  36490  poimirlem11  36494  poimirlem12  36495  poimirlem17  36500  poimirlem20  36503  poimirlem22  36505  poimirlem24  36507  poimirlem25  36508  poimirlem29  36512  poimirlem31  36514  mblfinlem2  36521  mbfposadd  36530  itg2addnc  36537  itgaddnclem2  36542  ftc1anclem5  36560  ftc1anclem8  36563  areacirc  36576  lcmineqlem4  40892  lcmineqlem18  40906  aks4d1p1p7  40934  aks4d1p3  40938  sticksstones10  40966  sticksstones12a  40968  metakunt29  41008  metakunt30  41009  3cubeslem2  41413  3cubeslem3r  41415  pell1qrgaplem  41601  jm2.19lem3  41720  jm2.25  41728  relexpaddss  42459  int-add01d  42926  binomcxplemnn0  43098  fperiodmullem  44003  xralrple3  44074  sumnnodd  44336  fprodaddrecnncnvlem  44615  ioodvbdlimc1lem2  44638  volioc  44678  volico  44689  stoweidlem11  44717  stoweidlem26  44732  stirlinglem12  44791  fourierdlem4  44817  fourierdlem42  44855  fourierdlem60  44872  fourierdlem61  44873  fourierdlem92  44904  fourierdlem107  44919  fouriersw  44937  etransclem24  44964  etransclem35  44975  hoidmvlelem2  45302  hspmbllem1  45332  sharhght  45571  deccarry  46009  nn0mnd  46579  pzriprnglem10  46804  altgsumbcALT  47019  itcovalpclem1  47346  eenglngeehlnmlem2  47414  line2y  47431  itschlc0xyqsol1  47442  itschlc0xyqsol  47443  2itscp  47457