Theorem addridd 11305

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

Syntax hints:   → wi 4   = wceq 1541   ∈ wcel 2110  (class class class)co 7341  ℂcc 10996  0cc0 10998   + caddc 11001

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2112  ax-9 2120  ax-10 2143  ax-11 2159  ax-12 2179  ax-ext 2702  ax-sep 5232  ax-nul 5242  ax-pow 5301  ax-pr 5368  ax-un 7663  ax-resscn 11055  ax-1cn 11056  ax-icn 11057  ax-addcl 11058  ax-addrcl 11059  ax-mulcl 11060  ax-mulrcl 11061  ax-mulcom 11062  ax-addass 11063  ax-mulass 11064  ax-distr 11065  ax-i2m1 11066  ax-1ne0 11067  ax-1rid 11068  ax-rnegex 11069  ax-rrecex 11070  ax-cnre 11071  ax-pre-lttri 11072  ax-pre-lttrn 11073  ax-pre-ltadd 11074

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-nf 1785  df-sb 2067  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 3394  df-v 3436  df-sbc 3740  df-csb 3849  df-dif 3903  df-un 3905  df-in 3907  df-ss 3917  df-nul 4282  df-if 4474  df-pw 4550  df-sn 4575  df-pr 4577  df-op 4581  df-uni 4858  df-br 5090  df-opab 5152  df-mpt 5171  df-id 5509  df-po 5522  df-so 5523  df-xp 5620  df-rel 5621  df-cnv 5622  df-co 5623  df-dm 5624  df-rn 5625  df-res 5626  df-ima 5627  df-iota 6433  df-fun 6479  df-fn 6480  df-f 6481  df-f1 6482  df-fo 6483  df-f1o 6484  df-fv 6485  df-ov 7344  df-er 8617  df-en 8865  df-dom 8866  df-sdom 8867  df-pnf 11140  df-mnf 11141  df-ltxr 11143

This theorem is referenced by:  ltaddneg  11321  subsub2  11381  negsub  11401  ltaddpos  11599  addge01  11619  add20  11621  nnge1  12145  nnnn0addcl  12403  un0addcl  12406  uzaddcl  12794  xaddrid  13132  fzosubel3  13618  expadd  14003  faclbnd4lem4  14195  faclbnd6  14198  hashgadd  14276  ccatrid  14487  pfxmpt  14578  pfxfv  14582  pfxswrd  14605  pfxccatin12lem1  14627  pfxccatin12lem2  14630  swrdccat3blem  14638  cshweqrep  14720  relexpaddg  14952  reim0b  15018  rereb  15019  immul2  15036  max0add  15209  iseraltlem2  15582  fsumsplit  15640  sumsplit  15667  binomfallfaclem2  15939  pwp1fsum  16294  bitsinv1lem  16344  sadadd2lem2  16353  sadcaddlem  16360  bezoutlem1  16442  pcadd  16793  pcadd2  16794  pcmpt  16796  vdwapun  16878  vdwlem1  16885  chnccat  18524  mulgnn0dir  19009  psgnunilem2  19400  sylow1lem1  19503  efginvrel2  19632  efgredleme  19648  efgcpbllemb  19660  frgpnabllem1  19778  regsumfsum  21365  pzriprnglem10  21420  regsumsupp  21552  mplcoe5  21968  psdmul  22074  xrsxmet  24718  reparphti  24916  reparphtiOLD  24917  cphpyth  25136  minveclem6  25354  ovolunnul  25421  voliunlem3  25473  ovolioo  25489  itg2splitlem  25669  itg2split  25670  itgrevallem1  25716  itgsplitioo  25759  ditgsplit  25782  dvnadd  25851  dvlipcn  25919  ply1divex  26062  dvntaylp  26299  ulmshft  26319  abelthlem6  26366  cosmpi  26417  sinppi  26418  sinhalfpip  26421  logrnaddcl  26503  affineequiv  26753  chordthmlem3  26764  atanlogaddlem  26843  atanlogsublem  26845  leibpi  26872  scvxcvx  26916  dmgmn0  26956  lgamgulmlem2  26960  lgambdd  26967  logexprlim  27156  2sqblem  27362  2sq2  27364  2sqnn  27370  dchrvmasum2if  27428  dchrvmasumlem  27454  axcontlem8  28942  elntg2  28956  crctcshlem4  29791  eupth2lem3lem6  30203  ipidsq  30680  minvecolem6  30852  normpyc  31116  pjspansn  31547  lnfnmuli  32014  hstoh  32202  indsumin  32833  archirngz  33148  constrrtlc2  33736  constrsslem  33744  2sqr3minply  33783  cos9thpiminply  33791  esumpfinvallem  34077  signsvtp  34586  signlem0  34590  fsum2dsub  34610  cvxpconn  35254  cvxsconn  35255  elmrsubrn  35532  faclim2  35760  fwddifn0  36177  fwddifnp1  36178  dnizeq0  36488  knoppndvlem6  36530  bj-bary1lem  37323  poimirlem1  37640  poimirlem5  37644  poimirlem6  37645  poimirlem7  37646  poimirlem11  37650  poimirlem12  37651  poimirlem17  37656  poimirlem20  37659  poimirlem22  37661  poimirlem24  37663  poimirlem25  37664  poimirlem29  37668  poimirlem31  37670  mblfinlem2  37677  mbfposadd  37686  itg2addnc  37693  itgaddnclem2  37698  ftc1anclem5  37716  ftc1anclem8  37719  areacirc  37732  lcmineqlem4  42044  lcmineqlem18  42058  aks4d1p1p7  42086  aks4d1p3  42090  posbezout  42112  primrootspoweq0  42118  sticksstones10  42167  sticksstones12a  42169  unitscyglem5  42211  3cubeslem2  42697  3cubeslem3r  42699  pell1qrgaplem  42885  jm2.19lem3  43003  jm2.25  43011  relexpaddss  43730  int-add01d  44196  binomcxplemnn0  44361  fperiodmullem  45323  xralrple3  45391  sumnnodd  45649  fprodaddrecnncnvlem  45926  ioodvbdlimc1lem2  45949  volioc  45989  volico  46000  stoweidlem11  46028  stoweidlem26  46043  stirlinglem12  46102  fourierdlem4  46128  fourierdlem42  46166  fourierdlem60  46183  fourierdlem61  46184  fourierdlem92  46215  fourierdlem107  46230  fouriersw  46248  etransclem24  46275  etransclem35  46286  hoidmvlelem2  46613  hspmbllem1  46643  sharhght  46882  deccarry  47321  nn0mnd  48189  altgsumbcALT  48363  itcovalpclem1  48681  eenglngeehlnmlem2  48749  line2y  48766  itschlc0xyqsol1  48777  itschlc0xyqsol  48778  2itscp  48792