Theorem addridd 11338

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

Syntax hints:   → wi 4   = wceq 1542   ∈ wcel 2114  (class class class)co 7361  ℂcc 11029  0cc0 11031   + caddc 11034

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 7683  ax-resscn 11088  ax-1cn 11089  ax-icn 11090  ax-addcl 11091  ax-addrcl 11092  ax-mulcl 11093  ax-mulrcl 11094  ax-mulcom 11095  ax-addass 11096  ax-mulass 11097  ax-distr 11098  ax-i2m1 11099  ax-1ne0 11100  ax-1rid 11101  ax-rnegex 11102  ax-rrecex 11103  ax-cnre 11104  ax-pre-lttri 11105  ax-pre-lttrn 11106  ax-pre-ltadd 11107

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 7364  df-er 8638  df-en 8889  df-dom 8890  df-sdom 8891  df-pnf 11173  df-mnf 11174  df-ltxr 11176

This theorem is referenced by:  ltaddneg  11354  subsub2  11414  negsub  11434  ltaddpos  11632  addge01  11652  add20  11654  nnge1  12178  nnnn0addcl  12436  un0addcl  12439  uzaddcl  12822  xaddrid  13161  fzosubel3  13647  expadd  14032  faclbnd4lem4  14224  faclbnd6  14227  hashgadd  14305  ccatrid  14516  pfxmpt  14607  pfxfv  14611  pfxswrd  14634  pfxccatin12lem1  14656  pfxccatin12lem2  14659  swrdccat3blem  14667  cshweqrep  14749  relexpaddg  14981  reim0b  15047  rereb  15048  immul2  15065  max0add  15238  iseraltlem2  15611  fsumsplit  15669  sumsplit  15696  binomfallfaclem2  15968  pwp1fsum  16323  bitsinv1lem  16373  sadadd2lem2  16382  sadcaddlem  16389  bezoutlem1  16471  pcadd  16822  pcadd2  16823  pcmpt  16825  vdwapun  16907  vdwlem1  16914  chnccat  18554  mulgnn0dir  19039  psgnunilem2  19429  sylow1lem1  19532  efginvrel2  19661  efgredleme  19677  efgcpbllemb  19689  frgpnabllem1  19807  regsumfsum  21395  pzriprnglem10  21450  regsumsupp  21582  mplcoe5  22000  psdmul  22114  xrsxmet  24759  reparphti  24957  reparphtiOLD  24958  cphpyth  25177  minveclem6  25395  ovolunnul  25462  voliunlem3  25514  ovolioo  25530  itg2splitlem  25710  itg2split  25711  itgrevallem1  25757  itgsplitioo  25800  ditgsplit  25823  dvnadd  25892  dvlipcn  25960  ply1divex  26103  dvntaylp  26340  ulmshft  26360  abelthlem6  26407  cosmpi  26458  sinppi  26459  sinhalfpip  26462  logrnaddcl  26544  affineequiv  26794  chordthmlem3  26805  atanlogaddlem  26884  atanlogsublem  26886  leibpi  26913  scvxcvx  26957  dmgmn0  26997  lgamgulmlem2  27001  lgambdd  27008  logexprlim  27197  2sqblem  27403  2sq2  27405  2sqnn  27411  dchrvmasum2if  27469  dchrvmasumlem  27495  axcontlem8  29049  elntg2  29063  crctcshlem4  29898  eupth2lem3lem6  30313  ipidsq  30790  minvecolem6  30962  normpyc  31226  pjspansn  31657  lnfnmuli  32124  hstoh  32312  indsumin  32946  archirngz  33275  constrrtlc2  33903  constrsslem  33911  2sqr3minply  33950  cos9thpiminply  33958  esumpfinvallem  34244  signsvtp  34753  signlem0  34757  fsum2dsub  34777  cvxpconn  35449  cvxsconn  35450  elmrsubrn  35727  faclim2  35955  fwddifn0  36371  fwddifnp1  36372  dnizeq0  36688  knoppndvlem6  36730  bj-bary1lem  37528  poimirlem1  37835  poimirlem5  37839  poimirlem6  37840  poimirlem7  37841  poimirlem11  37845  poimirlem12  37846  poimirlem17  37851  poimirlem20  37854  poimirlem22  37856  poimirlem24  37858  poimirlem25  37859  poimirlem29  37863  poimirlem31  37865  mblfinlem2  37872  mbfposadd  37881  itg2addnc  37888  itgaddnclem2  37893  ftc1anclem5  37911  ftc1anclem8  37914  areacirc  37927  lcmineqlem4  42365  lcmineqlem18  42379  aks4d1p1p7  42407  aks4d1p3  42411  posbezout  42433  primrootspoweq0  42439  sticksstones10  42488  sticksstones12a  42490  unitscyglem5  42532  3cubeslem2  43005  3cubeslem3r  43007  pell1qrgaplem  43193  jm2.19lem3  43311  jm2.25  43319  relexpaddss  44037  int-add01d  44503  binomcxplemnn0  44668  fperiodmullem  45628  xralrple3  45695  sumnnodd  45953  fprodaddrecnncnvlem  46230  ioodvbdlimc1lem2  46253  volioc  46293  volico  46304  stoweidlem11  46332  stoweidlem26  46347  stirlinglem12  46406  fourierdlem4  46432  fourierdlem42  46470  fourierdlem60  46487  fourierdlem61  46488  fourierdlem92  46519  fourierdlem107  46534  fouriersw  46552  etransclem24  46579  etransclem35  46590  hoidmvlelem2  46917  hspmbllem1  46947  sharhght  47186  deccarry  47634  nn0mnd  48502  altgsumbcALT  48676  itcovalpclem1  48993  eenglngeehlnmlem2  49061  line2y  49078  itschlc0xyqsol1  49089  itschlc0xyqsol  49090  2itscp  49104