Theorem addridd 11323

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

Syntax hints:   → wi 4   = wceq 1541   ∈ wcel 2113  (class class class)co 7355  ℂcc 11014  0cc0 11016   + caddc 11019

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 2115  ax-9 2123  ax-10 2146  ax-11 2162  ax-12 2182  ax-ext 2705  ax-sep 5238  ax-nul 5248  ax-pow 5307  ax-pr 5374  ax-un 7677  ax-resscn 11073  ax-1cn 11074  ax-icn 11075  ax-addcl 11076  ax-addrcl 11077  ax-mulcl 11078  ax-mulrcl 11079  ax-mulcom 11080  ax-addass 11081  ax-mulass 11082  ax-distr 11083  ax-i2m1 11084  ax-1ne0 11085  ax-1rid 11086  ax-rnegex 11087  ax-rrecex 11088  ax-cnre 11089  ax-pre-lttri 11090  ax-pre-lttrn 11091  ax-pre-ltadd 11092

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 2068  df-mo 2537  df-eu 2566  df-clab 2712  df-cleq 2725  df-clel 2808  df-nfc 2883  df-ne 2931  df-nel 3035  df-ral 3050  df-rex 3059  df-rab 3398  df-v 3440  df-sbc 3739  df-csb 3848  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-nul 4285  df-if 4477  df-pw 4553  df-sn 4578  df-pr 4580  df-op 4584  df-uni 4861  df-br 5096  df-opab 5158  df-mpt 5177  df-id 5516  df-po 5529  df-so 5530  df-xp 5627  df-rel 5628  df-cnv 5629  df-co 5630  df-dm 5631  df-rn 5632  df-res 5633  df-ima 5634  df-iota 6445  df-fun 6491  df-fn 6492  df-f 6493  df-f1 6494  df-fo 6495  df-f1o 6496  df-fv 6497  df-ov 7358  df-er 8631  df-en 8879  df-dom 8880  df-sdom 8881  df-pnf 11158  df-mnf 11159  df-ltxr 11161

This theorem is referenced by:  ltaddneg  11339  subsub2  11399  negsub  11419  ltaddpos  11617  addge01  11637  add20  11639  nnge1  12163  nnnn0addcl  12421  un0addcl  12424  uzaddcl  12812  xaddrid  13150  fzosubel3  13636  expadd  14021  faclbnd4lem4  14213  faclbnd6  14216  hashgadd  14294  ccatrid  14505  pfxmpt  14596  pfxfv  14600  pfxswrd  14623  pfxccatin12lem1  14645  pfxccatin12lem2  14648  swrdccat3blem  14656  cshweqrep  14738  relexpaddg  14970  reim0b  15036  rereb  15037  immul2  15054  max0add  15227  iseraltlem2  15600  fsumsplit  15658  sumsplit  15685  binomfallfaclem2  15957  pwp1fsum  16312  bitsinv1lem  16362  sadadd2lem2  16371  sadcaddlem  16378  bezoutlem1  16460  pcadd  16811  pcadd2  16812  pcmpt  16814  vdwapun  16896  vdwlem1  16903  chnccat  18542  mulgnn0dir  19027  psgnunilem2  19417  sylow1lem1  19520  efginvrel2  19649  efgredleme  19665  efgcpbllemb  19677  frgpnabllem1  19795  regsumfsum  21382  pzriprnglem10  21437  regsumsupp  21569  mplcoe5  21985  psdmul  22091  xrsxmet  24735  reparphti  24933  reparphtiOLD  24934  cphpyth  25153  minveclem6  25371  ovolunnul  25438  voliunlem3  25490  ovolioo  25506  itg2splitlem  25686  itg2split  25687  itgrevallem1  25733  itgsplitioo  25776  ditgsplit  25799  dvnadd  25868  dvlipcn  25936  ply1divex  26079  dvntaylp  26316  ulmshft  26336  abelthlem6  26383  cosmpi  26434  sinppi  26435  sinhalfpip  26438  logrnaddcl  26520  affineequiv  26770  chordthmlem3  26781  atanlogaddlem  26860  atanlogsublem  26862  leibpi  26889  scvxcvx  26933  dmgmn0  26973  lgamgulmlem2  26977  lgambdd  26984  logexprlim  27173  2sqblem  27379  2sq2  27381  2sqnn  27387  dchrvmasum2if  27445  dchrvmasumlem  27471  axcontlem8  28960  elntg2  28974  crctcshlem4  29809  eupth2lem3lem6  30224  ipidsq  30701  minvecolem6  30873  normpyc  31137  pjspansn  31568  lnfnmuli  32035  hstoh  32223  indsumin  32854  archirngz  33169  constrrtlc2  33757  constrsslem  33765  2sqr3minply  33804  cos9thpiminply  33812  esumpfinvallem  34098  signsvtp  34607  signlem0  34611  fsum2dsub  34631  cvxpconn  35297  cvxsconn  35298  elmrsubrn  35575  faclim2  35803  fwddifn0  36219  fwddifnp1  36220  dnizeq0  36530  knoppndvlem6  36572  bj-bary1lem  37365  poimirlem1  37671  poimirlem5  37675  poimirlem6  37676  poimirlem7  37677  poimirlem11  37681  poimirlem12  37682  poimirlem17  37687  poimirlem20  37690  poimirlem22  37692  poimirlem24  37694  poimirlem25  37695  poimirlem29  37699  poimirlem31  37701  mblfinlem2  37708  mbfposadd  37717  itg2addnc  37724  itgaddnclem2  37729  ftc1anclem5  37747  ftc1anclem8  37750  areacirc  37763  lcmineqlem4  42135  lcmineqlem18  42149  aks4d1p1p7  42177  aks4d1p3  42181  posbezout  42203  primrootspoweq0  42209  sticksstones10  42258  sticksstones12a  42260  unitscyglem5  42302  3cubeslem2  42792  3cubeslem3r  42794  pell1qrgaplem  42980  jm2.19lem3  43098  jm2.25  43106  relexpaddss  43825  int-add01d  44291  binomcxplemnn0  44456  fperiodmullem  45418  xralrple3  45486  sumnnodd  45744  fprodaddrecnncnvlem  46021  ioodvbdlimc1lem2  46044  volioc  46084  volico  46095  stoweidlem11  46123  stoweidlem26  46138  stirlinglem12  46197  fourierdlem4  46223  fourierdlem42  46261  fourierdlem60  46278  fourierdlem61  46279  fourierdlem92  46310  fourierdlem107  46325  fouriersw  46343  etransclem24  46370  etransclem35  46381  hoidmvlelem2  46708  hspmbllem1  46738  sharhght  46977  deccarry  47425  nn0mnd  48293  altgsumbcALT  48467  itcovalpclem1  48785  eenglngeehlnmlem2  48853  line2y  48870  itschlc0xyqsol1  48881  itschlc0xyqsol  48882  2itscp  48896