Theorem addridd 11461

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

Syntax hints:   → wi 4   = wceq 1540   ∈ wcel 2108  (class class class)co 7431  ℂcc 11153  0cc0 11155   + caddc 11158

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 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2157  ax-12 2177  ax-ext 2708  ax-sep 5296  ax-nul 5306  ax-pow 5365  ax-pr 5432  ax-un 7755  ax-resscn 11212  ax-1cn 11213  ax-icn 11214  ax-addcl 11215  ax-addrcl 11216  ax-mulcl 11217  ax-mulrcl 11218  ax-mulcom 11219  ax-addass 11220  ax-mulass 11221  ax-distr 11222  ax-i2m1 11223  ax-1ne0 11224  ax-1rid 11225  ax-rnegex 11226  ax-rrecex 11227  ax-cnre 11228  ax-pre-lttri 11229  ax-pre-lttrn 11230  ax-pre-ltadd 11231

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2065  df-mo 2540  df-eu 2569  df-clab 2715  df-cleq 2729  df-clel 2816  df-nfc 2892  df-ne 2941  df-nel 3047  df-ral 3062  df-rex 3071  df-rab 3437  df-v 3482  df-sbc 3789  df-csb 3900  df-dif 3954  df-un 3956  df-in 3958  df-ss 3968  df-nul 4334  df-if 4526  df-pw 4602  df-sn 4627  df-pr 4629  df-op 4633  df-uni 4908  df-br 5144  df-opab 5206  df-mpt 5226  df-id 5578  df-po 5592  df-so 5593  df-xp 5691  df-rel 5692  df-cnv 5693  df-co 5694  df-dm 5695  df-rn 5696  df-res 5697  df-ima 5698  df-iota 6514  df-fun 6563  df-fn 6564  df-f 6565  df-f1 6566  df-fo 6567  df-f1o 6568  df-fv 6569  df-ov 7434  df-er 8745  df-en 8986  df-dom 8987  df-sdom 8988  df-pnf 11297  df-mnf 11298  df-ltxr 11300

This theorem is referenced by:  ltaddneg  11477  subsub2  11537  negsub  11557  ltaddpos  11753  addge01  11773  add20  11775  nnge1  12294  nnnn0addcl  12556  un0addcl  12559  uzaddcl  12946  xaddrid  13283  fzosubel3  13765  expadd  14145  faclbnd4lem4  14335  faclbnd6  14338  hashgadd  14416  ccatrid  14625  pfxmpt  14716  pfxfv  14720  pfxswrd  14744  pfxccatin12lem1  14766  pfxccatin12lem2  14769  swrdccat3blem  14777  cshweqrep  14859  relexpaddg  15092  reim0b  15158  rereb  15159  immul2  15176  max0add  15349  iseraltlem2  15719  fsumsplit  15777  sumsplit  15804  binomfallfaclem2  16076  pwp1fsum  16428  bitsinv1lem  16478  sadadd2lem2  16487  sadcaddlem  16494  bezoutlem1  16576  pcadd  16927  pcadd2  16928  pcmpt  16930  vdwapun  17012  vdwlem1  17019  mulgnn0dir  19122  psgnunilem2  19513  sylow1lem1  19616  efginvrel2  19745  efgredleme  19761  efgcpbllemb  19773  frgpnabllem1  19891  regsumfsum  21453  pzriprnglem10  21501  regsumsupp  21640  mplcoe5  22058  psdmul  22170  xrsxmet  24831  reparphti  25029  reparphtiOLD  25030  cphpyth  25250  minveclem6  25468  ovolunnul  25535  voliunlem3  25587  ovolioo  25603  itg2splitlem  25783  itg2split  25784  itgrevallem1  25830  itgsplitioo  25873  ditgsplit  25896  dvnadd  25965  dvlipcn  26033  ply1divex  26176  dvntaylp  26413  ulmshft  26433  abelthlem6  26480  cosmpi  26530  sinppi  26531  sinhalfpip  26534  logrnaddcl  26616  affineequiv  26866  chordthmlem3  26877  atanlogaddlem  26956  atanlogsublem  26958  leibpi  26985  scvxcvx  27029  dmgmn0  27069  lgamgulmlem2  27073  lgambdd  27080  logexprlim  27269  2sqblem  27475  2sq2  27477  2sqnn  27483  dchrvmasum2if  27541  dchrvmasumlem  27567  axcontlem8  28986  elntg2  29000  crctcshlem4  29840  eupth2lem3lem6  30252  ipidsq  30729  minvecolem6  30901  normpyc  31165  pjspansn  31596  lnfnmuli  32063  hstoh  32251  indsumin  32847  archirngz  33196  constrrtlc2  33774  constrsslem  33782  2sqr3minply  33791  esumpfinvallem  34075  signsvtp  34598  signlem0  34602  fsum2dsub  34622  cvxpconn  35247  cvxsconn  35248  elmrsubrn  35525  faclim2  35748  fwddifn0  36165  fwddifnp1  36166  dnizeq0  36476  knoppndvlem6  36518  bj-bary1lem  37311  poimirlem1  37628  poimirlem5  37632  poimirlem6  37633  poimirlem7  37634  poimirlem11  37638  poimirlem12  37639  poimirlem17  37644  poimirlem20  37647  poimirlem22  37649  poimirlem24  37651  poimirlem25  37652  poimirlem29  37656  poimirlem31  37658  mblfinlem2  37665  mbfposadd  37674  itg2addnc  37681  itgaddnclem2  37686  ftc1anclem5  37704  ftc1anclem8  37707  areacirc  37720  lcmineqlem4  42033  lcmineqlem18  42047  aks4d1p1p7  42075  aks4d1p3  42079  posbezout  42101  primrootspoweq0  42107  sticksstones10  42156  sticksstones12a  42158  unitscyglem5  42200  metakunt29  42234  metakunt30  42235  3cubeslem2  42696  3cubeslem3r  42698  pell1qrgaplem  42884  jm2.19lem3  43003  jm2.25  43011  relexpaddss  43731  int-add01d  44197  binomcxplemnn0  44368  fperiodmullem  45315  xralrple3  45385  sumnnodd  45645  fprodaddrecnncnvlem  45924  ioodvbdlimc1lem2  45947  volioc  45987  volico  45998  stoweidlem11  46026  stoweidlem26  46041  stirlinglem12  46100  fourierdlem4  46126  fourierdlem42  46164  fourierdlem60  46181  fourierdlem61  46182  fourierdlem92  46213  fourierdlem107  46228  fouriersw  46246  etransclem24  46273  etransclem35  46284  hoidmvlelem2  46611  hspmbllem1  46641  sharhght  46880  deccarry  47323  nn0mnd  48095  altgsumbcALT  48269  itcovalpclem1  48591  eenglngeehlnmlem2  48659  line2y  48676  itschlc0xyqsol1  48687  itschlc0xyqsol  48688  2itscp  48702