Theorem addridd 11369

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

Syntax hints:   → wi 4   = wceq 1550   ∈ wcel 2132  (class class class)co 7381  ℂcc 11057  0cc0 11059   + caddc 11062

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1805  ax-4 1819  ax-5 1920  ax-6 1977  ax-7 2018  ax-8 2134  ax-9 2142  ax-10 2165  ax-11 2181  ax-12 2202  ax-ext 2724  ax-sep 5236  ax-nul 5246  ax-pow 5312  ax-pr 5380  ax-un 7703  ax-resscn 11116  ax-1cn 11117  ax-icn 11118  ax-addcl 11119  ax-addrcl 11120  ax-mulcl 11121  ax-mulrcl 11122  ax-mulcom 11123  ax-addass 11124  ax-mulass 11125  ax-distr 11126  ax-i2m1 11127  ax-1ne0 11128  ax-1rid 11129  ax-rnegex 11130  ax-rrecex 11131  ax-cnre 11132  ax-pre-lttri 11133  ax-pre-lttrn 11134  ax-pre-ltadd 11135

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 857  df-3or 1096  df-3an 1097  df-tru 1553  df-fal 1563  df-ex 1790  df-nf 1794  df-sb 2081  df-mo 2556  df-eu 2586  df-clab 2731  df-cleq 2744  df-clel 2827  df-nfc 2901  df-ne 2948  df-nel 3052  df-ral 3067  df-rex 3077  df-rab 3405  df-v 3446  df-sbc 3736  df-csb 3844  df-dif 3898  df-un 3900  df-in 3902  df-ss 3912  df-nul 4277  df-if 4471  df-pw 4547  df-sn 4573  df-pr 4575  df-op 4579  df-uni 4856  df-br 5091  df-opab 5153  df-mpt 5172  df-id 5531  df-po 5544  df-so 5545  df-xp 5642  df-rel 5643  df-cnv 5644  df-co 5645  df-dm 5646  df-rn 5647  df-res 5648  df-ima 5649  df-iota 6462  df-fun 6508  df-fn 6509  df-f 6510  df-f1 6511  df-fo 6512  df-f1o 6513  df-fv 6514  df-ov 7384  df-er 8662  df-en 8913  df-dom 8914  df-sdom 8915  df-pnf 11204  df-mnf 11205  df-ltxr 11207

This theorem is referenced by:  ltaddneg  11385  subsub2  11445  negsub  11465  ltaddpos  11663  addge01  11683  add20  11685  nnge1  12227  nnnn0addcl  12497  un0addcl  12500  uzaddcl  12891  xaddrid  13230  fzosubel3  13718  expadd  14103  faclbnd4lem4  14295  faclbnd6  14298  hashgadd  14376  ccatrid  14587  pfxmpt  14678  pfxfv  14682  pfxswrd  14705  pfxccatin12lem1  14727  pfxccatin12lem2  14730  swrdccat3blem  14738  cshweqrep  14820  relexpaddg  15052  reim0b  15118  rereb  15119  immul2  15136  max0add  15309  iseraltlem2  15682  fsumsplit  15740  sumsplit  15767  binomfallfaclem2  16042  pwp1fsum  16397  bitsinv1lem  16447  sadadd2lem2  16456  sadcaddlem  16463  bezoutlem1  16545  pcadd  16897  pcadd2  16898  pcmpt  16900  vdwapun  16982  vdwlem1  16989  chnccat  18630  mulgnn0dir  19118  psgnunilem2  19507  sylow1lem1  19610  efginvrel2  19739  efgredleme  19755  efgcpbllemb  19767  frgpnabllem1  19885  regsumfsum  21456  pzriprnglem10  21511  regsumsupp  21643  mplcoe5  22062  psdmul  22200  xrsxmet  24839  reparphti  25028  cphpyth  25247  minveclem6  25465  ovolunnul  25531  voliunlem3  25583  ovolioo  25599  itg2splitlem  25779  itg2split  25780  itgrevallem1  25826  itgsplitioo  25869  ditgsplit  25892  dvnadd  25960  dvlipcn  26025  ply1divex  26166  dvntaylp  26400  ulmshft  26419  abelthlem6  26465  cosmpi  26519  sinppi  26520  sinhalfpip  26523  logrnaddcl  26605  affineequiv  26854  chordthmlem3  26865  atanlogaddlem  26944  atanlogsublem  26946  leibpi  26973  scvxcvx  27016  dmgmn0  27056  lgamgulmlem2  27060  lgambdd  27067  logexprlim  27255  2sqblem  27461  2sq2  27463  2sqnn  27469  dchrvmasum2if  27527  dchrvmasumlem  27553  axcontlem8  29107  elntg2  29121  crctcshlem4  29955  eupth2lem3lem6  30370  ipidsq  30848  minvecolem6  31020  normpyc  31284  pjspansn  31715  lnfnmuli  32182  hstoh  32370  indsumin  32989  archirngz  33319  constrrtlc2  33974  constrsslem  33982  2sqr3minply  34021  cos9thpiminply  34029  esumpfinvallem  34315  signsvtp  34824  signlem0  34828  fsum2dsub  34848  cvxpconn  35530  cvxsconn  35531  elmrsubrn  35808  faclim2  36036  fwddifn0  36452  fwddifnp1  36453  dnizeq0  36851  knoppndvlem6  36893  bj-bary1lem  37740  poimirlem1  38058  poimirlem5  38062  poimirlem6  38063  poimirlem7  38064  poimirlem11  38068  poimirlem12  38069  poimirlem17  38074  poimirlem20  38077  poimirlem22  38079  poimirlem24  38081  poimirlem25  38082  poimirlem29  38086  poimirlem31  38088  mblfinlem2  38095  mbfposadd  38104  itg2addnc  38111  itgaddnclem2  38116  ftc1anclem5  38134  ftc1anclem8  38137  areacirc  38150  lcmineqlem4  42587  lcmineqlem18  42601  aks4d1p1p7  42629  aks4d1p3  42633  posbezout  42655  primrootspoweq0  42661  sticksstones10  42710  sticksstones12a  42712  unitscyglem5  42754  3cubeslem2  43204  3cubeslem3r  43206  pell1qrgaplem  43388  jm2.19lem3  43506  jm2.25  43514  relexpaddss  44232  int-add01d  44698  binomcxplemnn0  44863  fperiodmullem  45820  xralrple3  45887  sumnnodd  46144  fprodaddrecnncnvlem  46421  ioodvbdlimc1lem2  46444  volioc  46484  volico  46495  stoweidlem11  46523  stoweidlem26  46538  stirlinglem12  46597  fourierdlem4  46623  fourierdlem42  46661  fourierdlem60  46678  fourierdlem61  46679  fourierdlem92  46710  fourierdlem107  46725  fouriersw  46743  etransclem24  46770  etransclem35  46781  hoidmvlelem2  47108  hspmbllem1  47138  sharhght  47377  deccarry  47843  flmrecm1  47875  nn0mnd  48739  altgsumbcALT  48913  itcovalpclem1  49230  eenglngeehlnmlem2  49298  line2y  49315  itschlc0xyqsol1  49326  itschlc0xyqsol  49327  2itscp  49341