Theorem addridd 11452

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

Syntax hints:   → wi 4   = wceq 1533   ∈ wcel 2098  (class class class)co 7426  ℂcc 11144  0cc0 11146   + caddc 11149

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-10 2129  ax-11 2146  ax-12 2166  ax-ext 2699  ax-sep 5303  ax-nul 5310  ax-pow 5369  ax-pr 5433  ax-un 7746  ax-resscn 11203  ax-1cn 11204  ax-icn 11205  ax-addcl 11206  ax-addrcl 11207  ax-mulcl 11208  ax-mulrcl 11209  ax-mulcom 11210  ax-addass 11211  ax-mulass 11212  ax-distr 11213  ax-i2m1 11214  ax-1ne0 11215  ax-1rid 11216  ax-rnegex 11217  ax-rrecex 11218  ax-cnre 11219  ax-pre-lttri 11220  ax-pre-lttrn 11221  ax-pre-ltadd 11222

This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-3or 1085  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-nf 1778  df-sb 2060  df-mo 2529  df-eu 2558  df-clab 2706  df-cleq 2720  df-clel 2806  df-nfc 2881  df-ne 2938  df-nel 3044  df-ral 3059  df-rex 3068  df-rab 3431  df-v 3475  df-sbc 3779  df-csb 3895  df-dif 3952  df-un 3954  df-in 3956  df-ss 3966  df-nul 4327  df-if 4533  df-pw 4608  df-sn 4633  df-pr 4635  df-op 4639  df-uni 4913  df-br 5153  df-opab 5215  df-mpt 5236  df-id 5580  df-po 5594  df-so 5595  df-xp 5688  df-rel 5689  df-cnv 5690  df-co 5691  df-dm 5692  df-rn 5693  df-res 5694  df-ima 5695  df-iota 6505  df-fun 6555  df-fn 6556  df-f 6557  df-f1 6558  df-fo 6559  df-f1o 6560  df-fv 6561  df-ov 7429  df-er 8731  df-en 8971  df-dom 8972  df-sdom 8973  df-pnf 11288  df-mnf 11289  df-ltxr 11291

This theorem is referenced by:  ltaddneg  11467  subsub2  11526  negsub  11546  ltaddpos  11742  addge01  11762  add20  11764  nnge1  12278  nnnn0addcl  12540  un0addcl  12543  uzaddcl  12926  xaddrid  13260  fzosubel3  13733  expadd  14109  faclbnd4lem4  14295  faclbnd6  14298  hashgadd  14376  ccatrid  14577  pfxmpt  14668  pfxfv  14672  pfxswrd  14696  pfxccatin12lem1  14718  pfxccatin12lem2  14721  swrdccat3blem  14729  cshweqrep  14811  relexpaddg  15040  reim0b  15106  rereb  15107  immul2  15124  max0add  15297  iseraltlem2  15669  fsumsplit  15727  sumsplit  15754  binomfallfaclem2  16024  pwp1fsum  16375  bitsinv1lem  16423  sadadd2lem2  16432  sadcaddlem  16439  bezoutlem1  16522  pcadd  16865  pcadd2  16866  pcmpt  16868  vdwapun  16950  vdwlem1  16957  mulgnn0dir  19066  psgnunilem2  19457  sylow1lem1  19560  efginvrel2  19689  efgredleme  19705  efgcpbllemb  19717  frgpnabllem1  19835  regsumfsum  21375  pzriprnglem10  21423  regsumsupp  21561  mplcoe5  21985  psdmul  22097  xrsxmet  24745  reparphti  24943  reparphtiOLD  24944  cphpyth  25164  minveclem6  25382  ovolunnul  25449  voliunlem3  25501  ovolioo  25517  itg2splitlem  25698  itg2split  25699  itgrevallem1  25744  itgsplitioo  25787  ditgsplit  25810  dvnadd  25879  dvlipcn  25947  ply1divex  26092  dvntaylp  26326  ulmshft  26346  abelthlem6  26393  cosmpi  26443  sinppi  26444  sinhalfpip  26447  logrnaddcl  26528  affineequiv  26775  chordthmlem3  26786  atanlogaddlem  26865  atanlogsublem  26867  leibpi  26894  scvxcvx  26938  dmgmn0  26978  lgamgulmlem2  26982  lgambdd  26989  logexprlim  27178  2sqblem  27384  2sq2  27386  2sqnn  27392  dchrvmasum2if  27450  dchrvmasumlem  27476  axcontlem8  28802  elntg2  28816  crctcshlem4  29651  eupth2lem3lem6  30063  ipidsq  30540  minvecolem6  30712  normpyc  30976  pjspansn  31407  lnfnmuli  31874  hstoh  32062  archirngz  32918  indsumin  33674  esumpfinvallem  33726  signsvtp  34248  signlem0  34252  fsum2dsub  34272  cvxpconn  34885  cvxsconn  34886  elmrsubrn  35163  faclim2  35375  fwddifn0  35793  fwddifnp1  35794  dnizeq0  35983  knoppndvlem6  36025  bj-bary1lem  36822  poimirlem1  37127  poimirlem5  37131  poimirlem6  37132  poimirlem7  37133  poimirlem11  37137  poimirlem12  37138  poimirlem17  37143  poimirlem20  37146  poimirlem22  37148  poimirlem24  37150  poimirlem25  37151  poimirlem29  37155  poimirlem31  37157  mblfinlem2  37164  mbfposadd  37173  itg2addnc  37180  itgaddnclem2  37185  ftc1anclem5  37203  ftc1anclem8  37206  areacirc  37219  lcmineqlem4  41535  lcmineqlem18  41549  aks4d1p1p7  41577  aks4d1p3  41581  posbezout  41603  primrootspoweq0  41609  sticksstones10  41659  sticksstones12a  41661  metakunt29  41717  metakunt30  41718  3cubeslem2  42136  3cubeslem3r  42138  pell1qrgaplem  42324  jm2.19lem3  42443  jm2.25  42451  relexpaddss  43179  int-add01d  43645  binomcxplemnn0  43817  fperiodmullem  44714  xralrple3  44785  sumnnodd  45047  fprodaddrecnncnvlem  45326  ioodvbdlimc1lem2  45349  volioc  45389  volico  45400  stoweidlem11  45428  stoweidlem26  45443  stirlinglem12  45502  fourierdlem4  45528  fourierdlem42  45566  fourierdlem60  45583  fourierdlem61  45584  fourierdlem92  45615  fourierdlem107  45630  fouriersw  45648  etransclem24  45675  etransclem35  45686  hoidmvlelem2  46013  hspmbllem1  46043  sharhght  46282  deccarry  46720  nn0mnd  47319  altgsumbcALT  47495  itcovalpclem1  47821  eenglngeehlnmlem2  47889  line2y  47906  itschlc0xyqsol1  47917  itschlc0xyqsol  47918  2itscp  47932