Theorem addridd 11409

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

Syntax hints:   → wi 4   = wceq 1568   ∈ wcel 2141  (class class class)co 7410  ℂcc 11097  0cc0 11099   + caddc 11102

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1823  ax-4 1837  ax-5 1938  ax-6 1995  ax-7 2036  ax-8 2143  ax-9 2151  ax-10 2174  ax-11 2190  ax-12 2211  ax-ext 2733  ax-sep 5256  ax-nul 5268  ax-pow 5336  ax-pr 5404  ax-un 7732  ax-resscn 11156  ax-1cn 11157  ax-icn 11158  ax-addcl 11159  ax-addrcl 11160  ax-mulcl 11161  ax-mulrcl 11162  ax-mulcom 11163  ax-addass 11164  ax-mulass 11165  ax-distr 11166  ax-i2m1 11167  ax-1ne0 11168  ax-1rid 11169  ax-rnegex 11170  ax-rrecex 11171  ax-cnre 11172  ax-pre-lttri 11173  ax-pre-lttrn 11174  ax-pre-ltadd 11175

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3or 1102  df-3an 1103  df-tru 1571  df-fal 1581  df-ex 1808  df-nf 1812  df-sb 2095  df-mo 2565  df-eu 2595  df-clab 2740  df-cleq 2753  df-clel 2836  df-nfc 2910  df-ne 2957  df-nel 3063  df-ral 3078  df-rex 3088  df-rab 3415  df-v 3455  df-sbc 3744  df-csb 3853  df-dif 3907  df-un 3909  df-in 3911  df-ss 3921  df-nul 4286  df-if 4487  df-pw 4563  df-sn 4589  df-pr 4591  df-op 4595  df-uni 4872  df-br 5109  df-opab 5173  df-mpt 5192  df-id 5556  df-po 5569  df-so 5570  df-xp 5667  df-rel 5668  df-cnv 5669  df-co 5670  df-dm 5671  df-rn 5672  df-res 5673  df-ima 5674  df-iota 6492  df-fun 6538  df-fn 6539  df-f 6540  df-f1 6541  df-fo 6542  df-f1o 6543  df-fv 6544  df-ov 7413  df-er 8693  df-en 8943  df-dom 8944  df-sdom 8945  df-pnf 11244  df-mnf 11245  df-ltxr 11247

This theorem is referenced by:  ltaddneg  11425  subsub2  11485  negsub  11505  ltaddpos  11703  addge01  11723  add20  11725  nnge1  12263  nnnn0addcl  12533  un0addcl  12536  uzaddcl  12927  xaddrid  13266  fzosubel3  13754  expadd  14139  faclbnd4lem4  14331  faclbnd6  14334  hashgadd  14412  ccatrid  14624  pfxmpt  14715  pfxfv  14719  pfxswrd  14742  pfxccatin12lem1  14764  pfxccatin12lem2  14767  swrdccat3blem  14775  cshweqrep  14857  relexpaddg  15089  reim0b  15169  rereb  15170  immul2  15187  max0add  15360  iseraltlem2  15733  fsumsplit  15791  sumsplit  15818  binomfallfaclem2  16093  pwp1fsum  16448  bitsinv1lem  16498  sadadd2lem2  16507  sadcaddlem  16514  bezoutlem1  16596  pcadd  16948  pcadd2  16949  pcmpt  16951  vdwapun  17033  vdwlem1  17040  chnccat  18681  mulgnn0dir  19169  psgnunilem2  19564  sylow1lem1  19667  efginvrel2  19796  efgredleme  19812  efgcpbllemb  19824  frgpnabllem1  19942  regsumfsum  21564  pzriprnglem10  21619  regsumsupp  21751  mplcoe5  22170  psdmul  22308  xrsxmet  24946  reparphti  25135  cphpyth  25354  minveclem6  25572  ovolunnul  25638  voliunlem3  25690  ovolioo  25706  itg2splitlem  25886  itg2split  25887  itgrevallem1  25933  itgsplitioo  25976  ditgsplit  25999  dvnadd  26067  dvlipcn  26132  ply1divex  26273  dvntaylp  26510  ulmshft  26529  abelthlem6  26575  cosmpi  26629  sinppi  26630  sinhalfpip  26633  logrnaddcl  26715  affineequiv  26964  chordthmlem3  26975  atanlogaddlem  27054  atanlogsublem  27056  leibpi  27083  scvxcvx  27126  dmgmn0  27166  lgamgulmlem2  27170  lgambdd  27177  logexprlim  27365  2sqblem  27571  2sq2  27573  2sqnn  27579  dchrvmasum2if  27637  dchrvmasumlem  27663  axcontlem8  29287  elntg2  29301  crctcshlem4  30135  eupth2lem3lem6  30550  ipidsq  31028  minvecolem6  31200  normpyc  31464  pjspansn  31895  lnfnmuli  32362  hstoh  32550  indsumin  33147  archirngz  33475  constrrtlc2  34089  constrsslem  34097  2sqr3minply  34136  cos9thpiminply  34144  esumpfinvallem  34430  signsvtp  34936  signlem0  34940  fsum2dsub  34960  cvxpconn  35688  cvxsconn  35689  elmrsubrn  35966  faclim2  36194  fwddifn0  36610  fwddifnp1  36611  dnizeq0  37008  knoppndvlem6  37050  bj-bary1lem  37898  poimirlem1  38216  poimirlem5  38220  poimirlem6  38221  poimirlem7  38222  poimirlem11  38226  poimirlem12  38227  poimirlem17  38232  poimirlem20  38235  poimirlem22  38237  poimirlem24  38239  poimirlem25  38240  poimirlem29  38244  poimirlem31  38246  mblfinlem2  38253  mbfposadd  38262  itg2addnc  38269  itgaddnclem2  38274  ftc1anclem5  38292  ftc1anclem8  38295  areacirc  38308  lcmineqlem4  42745  lcmineqlem18  42759  aks4d1p1p7  42787  aks4d1p3  42791  posbezout  42813  primrootspoweq0  42819  sticksstones10  42868  sticksstones12a  42870  unitscyglem5  42912  3cubeslem2  43364  3cubeslem3r  43366  pell1qrgaplem  43548  jm2.19lem3  43666  jm2.25  43674  relexpaddss  44392  int-add01d  44858  binomcxplemnn0  45007  fperiodmullem  45970  xralrple3  46037  sumnnodd  46294  fprodaddrecnncnvlem  46571  ioodvbdlimc1lem2  46594  volioc  46634  volico  46645  stoweidlem11  46673  stoweidlem26  46688  stirlinglem12  46747  fourierdlem4  46773  fourierdlem42  46811  fourierdlem60  46828  fourierdlem61  46829  fourierdlem92  46860  fourierdlem107  46875  fouriersw  46893  etransclem24  46920  etransclem35  46931  hoidmvlelem2  47258  hspmbllem1  47288  sharhght  47527  deccarry  47993  flmrecm1  48025  nn0mnd  48889  altgsumbcALT  49078  itcovalpclem1  49395  eenglngeehlnmlem2  49463  line2y  49480  itschlc0xyqsol1  49491  itschlc0xyqsol  49492  2itscp  49506