Theorem addridd 11337

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

Syntax hints:   → wi 4   = wceq 1542   ∈ wcel 2114  (class class class)co 7360  ℂcc 11028  0cc0 11030   + caddc 11033

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2709  ax-sep 5242  ax-nul 5252  ax-pow 5311  ax-pr 5378  ax-un 7682  ax-resscn 11087  ax-1cn 11088  ax-icn 11089  ax-addcl 11090  ax-addrcl 11091  ax-mulcl 11092  ax-mulrcl 11093  ax-mulcom 11094  ax-addass 11095  ax-mulass 11096  ax-distr 11097  ax-i2m1 11098  ax-1ne0 11099  ax-1rid 11100  ax-rnegex 11101  ax-rrecex 11102  ax-cnre 11103  ax-pre-lttri 11104  ax-pre-lttrn 11105  ax-pre-ltadd 11106

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2540  df-eu 2570  df-clab 2716  df-cleq 2729  df-clel 2812  df-nfc 2886  df-ne 2934  df-nel 3038  df-ral 3053  df-rex 3062  df-rab 3401  df-v 3443  df-sbc 3742  df-csb 3851  df-dif 3905  df-un 3907  df-in 3909  df-ss 3919  df-nul 4287  df-if 4481  df-pw 4557  df-sn 4582  df-pr 4584  df-op 4588  df-uni 4865  df-br 5100  df-opab 5162  df-mpt 5181  df-id 5520  df-po 5533  df-so 5534  df-xp 5631  df-rel 5632  df-cnv 5633  df-co 5634  df-dm 5635  df-rn 5636  df-res 5637  df-ima 5638  df-iota 6449  df-fun 6495  df-fn 6496  df-f 6497  df-f1 6498  df-fo 6499  df-f1o 6500  df-fv 6501  df-ov 7363  df-er 8637  df-en 8888  df-dom 8889  df-sdom 8890  df-pnf 11172  df-mnf 11173  df-ltxr 11175

This theorem is referenced by:  ltaddneg  11353  subsub2  11413  negsub  11433  ltaddpos  11631  addge01  11651  add20  11653  nnge1  12177  nnnn0addcl  12435  un0addcl  12438  uzaddcl  12821  xaddrid  13160  fzosubel3  13646  expadd  14031  faclbnd4lem4  14223  faclbnd6  14226  hashgadd  14304  ccatrid  14515  pfxmpt  14606  pfxfv  14610  pfxswrd  14633  pfxccatin12lem1  14655  pfxccatin12lem2  14658  swrdccat3blem  14666  cshweqrep  14748  relexpaddg  14980  reim0b  15046  rereb  15047  immul2  15064  max0add  15237  iseraltlem2  15610  fsumsplit  15668  sumsplit  15695  binomfallfaclem2  15967  pwp1fsum  16322  bitsinv1lem  16372  sadadd2lem2  16381  sadcaddlem  16388  bezoutlem1  16470  pcadd  16821  pcadd2  16822  pcmpt  16824  vdwapun  16906  vdwlem1  16913  chnccat  18553  mulgnn0dir  19038  psgnunilem2  19428  sylow1lem1  19531  efginvrel2  19660  efgredleme  19676  efgcpbllemb  19688  frgpnabllem1  19806  regsumfsum  21394  pzriprnglem10  21449  regsumsupp  21581  mplcoe5  21999  psdmul  22113  xrsxmet  24758  reparphti  24956  reparphtiOLD  24957  cphpyth  25176  minveclem6  25394  ovolunnul  25461  voliunlem3  25513  ovolioo  25529  itg2splitlem  25709  itg2split  25710  itgrevallem1  25756  itgsplitioo  25799  ditgsplit  25822  dvnadd  25891  dvlipcn  25959  ply1divex  26102  dvntaylp  26339  ulmshft  26359  abelthlem6  26406  cosmpi  26457  sinppi  26458  sinhalfpip  26461  logrnaddcl  26543  affineequiv  26793  chordthmlem3  26804  atanlogaddlem  26883  atanlogsublem  26885  leibpi  26912  scvxcvx  26956  dmgmn0  26996  lgamgulmlem2  27000  lgambdd  27007  logexprlim  27196  2sqblem  27402  2sq2  27404  2sqnn  27410  dchrvmasum2if  27468  dchrvmasumlem  27494  axcontlem8  29027  elntg2  29041  crctcshlem4  29876  eupth2lem3lem6  30291  ipidsq  30768  minvecolem6  30940  normpyc  31204  pjspansn  31635  lnfnmuli  32102  hstoh  32290  indsumin  32924  archirngz  33252  constrrtlc2  33871  constrsslem  33879  2sqr3minply  33918  cos9thpiminply  33926  esumpfinvallem  34212  signsvtp  34721  signlem0  34725  fsum2dsub  34745  cvxpconn  35417  cvxsconn  35418  elmrsubrn  35695  faclim2  35923  fwddifn0  36339  fwddifnp1  36340  dnizeq0  36650  knoppndvlem6  36692  bj-bary1lem  37486  poimirlem1  37793  poimirlem5  37797  poimirlem6  37798  poimirlem7  37799  poimirlem11  37803  poimirlem12  37804  poimirlem17  37809  poimirlem20  37812  poimirlem22  37814  poimirlem24  37816  poimirlem25  37817  poimirlem29  37821  poimirlem31  37823  mblfinlem2  37830  mbfposadd  37839  itg2addnc  37846  itgaddnclem2  37851  ftc1anclem5  37869  ftc1anclem8  37872  areacirc  37885  lcmineqlem4  42323  lcmineqlem18  42337  aks4d1p1p7  42365  aks4d1p3  42369  posbezout  42391  primrootspoweq0  42397  sticksstones10  42446  sticksstones12a  42448  unitscyglem5  42490  3cubeslem2  42963  3cubeslem3r  42965  pell1qrgaplem  43151  jm2.19lem3  43269  jm2.25  43277  relexpaddss  43995  int-add01d  44461  binomcxplemnn0  44626  fperiodmullem  45587  xralrple3  45654  sumnnodd  45912  fprodaddrecnncnvlem  46189  ioodvbdlimc1lem2  46212  volioc  46252  volico  46263  stoweidlem11  46291  stoweidlem26  46306  stirlinglem12  46365  fourierdlem4  46391  fourierdlem42  46429  fourierdlem60  46446  fourierdlem61  46447  fourierdlem92  46478  fourierdlem107  46493  fouriersw  46511  etransclem24  46538  etransclem35  46549  hoidmvlelem2  46876  hspmbllem1  46906  sharhght  47145  deccarry  47593  nn0mnd  48461  altgsumbcALT  48635  itcovalpclem1  48952  eenglngeehlnmlem2  49020  line2y  49037  itschlc0xyqsol1  49048  itschlc0xyqsol  49049  2itscp  49063