Theorem addridd 11394

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

Syntax hints:   → wi 4   = wceq 1561   ∈ wcel 2143  (class class class)co 7396  ℂcc 11082  0cc0 11084   + caddc 11087

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1816  ax-4 1830  ax-5 1931  ax-6 1988  ax-7 2029  ax-8 2145  ax-9 2153  ax-10 2176  ax-11 2192  ax-12 2213  ax-ext 2735  ax-sep 5247  ax-nul 5257  ax-pow 5323  ax-pr 5391  ax-un 7718  ax-resscn 11141  ax-1cn 11142  ax-icn 11143  ax-addcl 11144  ax-addrcl 11145  ax-mulcl 11146  ax-mulrcl 11147  ax-mulcom 11148  ax-addass 11149  ax-mulass 11150  ax-distr 11151  ax-i2m1 11152  ax-1ne0 11153  ax-1rid 11154  ax-rnegex 11155  ax-rrecex 11156  ax-cnre 11157  ax-pre-lttri 11158  ax-pre-lttrn 11159  ax-pre-ltadd 11160

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-3or 1100  df-3an 1101  df-tru 1564  df-fal 1574  df-ex 1801  df-nf 1805  df-sb 2092  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2838  df-nfc 2912  df-ne 2959  df-nel 3063  df-ral 3078  df-rex 3088  df-rab 3416  df-v 3457  df-sbc 3746  df-csb 3854  df-dif 3908  df-un 3910  df-in 3912  df-ss 3922  df-nul 4287  df-if 4482  df-pw 4558  df-sn 4584  df-pr 4586  df-op 4590  df-uni 4867  df-br 5102  df-opab 5164  df-mpt 5183  df-id 5543  df-po 5556  df-so 5557  df-xp 5654  df-rel 5655  df-cnv 5656  df-co 5657  df-dm 5658  df-rn 5659  df-res 5660  df-ima 5661  df-iota 6477  df-fun 6523  df-fn 6524  df-f 6525  df-f1 6526  df-fo 6527  df-f1o 6528  df-fv 6529  df-ov 7399  df-er 8678  df-en 8928  df-dom 8929  df-sdom 8930  df-pnf 11229  df-mnf 11230  df-ltxr 11232

This theorem is referenced by:  ltaddneg  11410  subsub2  11470  negsub  11490  ltaddpos  11688  addge01  11708  add20  11710  nnge1  12251  nnnn0addcl  12521  un0addcl  12524  uzaddcl  12915  xaddrid  13254  fzosubel3  13742  expadd  14127  faclbnd4lem4  14319  faclbnd6  14322  hashgadd  14400  ccatrid  14611  pfxmpt  14702  pfxfv  14706  pfxswrd  14729  pfxccatin12lem1  14751  pfxccatin12lem2  14754  swrdccat3blem  14762  cshweqrep  14844  relexpaddg  15076  reim0b  15156  rereb  15157  immul2  15174  max0add  15347  iseraltlem2  15720  fsumsplit  15778  sumsplit  15805  binomfallfaclem2  16080  pwp1fsum  16435  bitsinv1lem  16485  sadadd2lem2  16494  sadcaddlem  16501  bezoutlem1  16583  pcadd  16935  pcadd2  16936  pcmpt  16938  vdwapun  17020  vdwlem1  17027  chnccat  18668  mulgnn0dir  19156  psgnunilem2  19545  sylow1lem1  19648  efginvrel2  19777  efgredleme  19793  efgcpbllemb  19805  frgpnabllem1  19923  regsumfsum  21494  pzriprnglem10  21549  regsumsupp  21681  mplcoe5  22100  psdmul  22238  xrsxmet  24877  reparphti  25066  cphpyth  25285  minveclem6  25503  ovolunnul  25569  voliunlem3  25621  ovolioo  25637  itg2splitlem  25817  itg2split  25818  itgrevallem1  25864  itgsplitioo  25907  ditgsplit  25930  dvnadd  25998  dvlipcn  26063  ply1divex  26204  dvntaylp  26441  ulmshft  26460  abelthlem6  26506  cosmpi  26560  sinppi  26561  sinhalfpip  26564  logrnaddcl  26646  affineequiv  26895  chordthmlem3  26906  atanlogaddlem  26985  atanlogsublem  26987  leibpi  27014  scvxcvx  27057  dmgmn0  27097  lgamgulmlem2  27101  lgambdd  27108  logexprlim  27296  2sqblem  27502  2sq2  27504  2sqnn  27510  dchrvmasum2if  27568  dchrvmasumlem  27594  axcontlem8  29179  elntg2  29193  crctcshlem4  30027  eupth2lem3lem6  30442  ipidsq  30920  minvecolem6  31092  normpyc  31356  pjspansn  31787  lnfnmuli  32254  hstoh  32442  indsumin  33045  archirngz  33375  constrrtlc2  34032  constrsslem  34040  2sqr3minply  34079  cos9thpiminply  34087  esumpfinvallem  34373  signsvtp  34879  signlem0  34883  fsum2dsub  34903  cvxpconn  35597  cvxsconn  35598  elmrsubrn  35875  faclim2  36103  fwddifn0  36519  fwddifnp1  36520  dnizeq0  36918  knoppndvlem6  36960  bj-bary1lem  37807  poimirlem1  38125  poimirlem5  38129  poimirlem6  38130  poimirlem7  38131  poimirlem11  38135  poimirlem12  38136  poimirlem17  38141  poimirlem20  38144  poimirlem22  38146  poimirlem24  38148  poimirlem25  38149  poimirlem29  38153  poimirlem31  38155  mblfinlem2  38162  mbfposadd  38171  itg2addnc  38178  itgaddnclem2  38183  ftc1anclem5  38201  ftc1anclem8  38204  areacirc  38217  lcmineqlem4  42654  lcmineqlem18  42668  aks4d1p1p7  42696  aks4d1p3  42700  posbezout  42722  primrootspoweq0  42728  sticksstones10  42777  sticksstones12a  42779  unitscyglem5  42821  3cubeslem2  43271  3cubeslem3r  43273  pell1qrgaplem  43455  jm2.19lem3  43573  jm2.25  43581  relexpaddss  44299  int-add01d  44765  binomcxplemnn0  44916  fperiodmullem  45873  xralrple3  45940  sumnnodd  46197  fprodaddrecnncnvlem  46474  ioodvbdlimc1lem2  46497  volioc  46537  volico  46548  stoweidlem11  46576  stoweidlem26  46591  stirlinglem12  46650  fourierdlem4  46676  fourierdlem42  46714  fourierdlem60  46731  fourierdlem61  46732  fourierdlem92  46763  fourierdlem107  46778  fouriersw  46796  etransclem24  46823  etransclem35  46834  hoidmvlelem2  47161  hspmbllem1  47191  sharhght  47430  deccarry  47896  flmrecm1  47928  nn0mnd  48792  altgsumbcALT  48966  itcovalpclem1  49283  eenglngeehlnmlem2  49351  line2y  49368  itschlc0xyqsol1  49379  itschlc0xyqsol  49380  2itscp  49394