Theorem addridd 11437

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

This proof depends on syntax axioms:   → wi 4   = wceq 1570   ∈ wcel 2145  (class class class)co 7416  ℂcc 11125  0cc0 11127   + caddc 11130

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2215  ax-ext 2734  ax-sep 5255  ax-nul 5267  ax-pow 5334  ax-pr 5402  ax-un 7739  ax-resscn 11184  ax-1cn 11185  ax-icn 11186  ax-addcl 11187  ax-addrcl 11188  ax-mulcl 11189  ax-mulrcl 11190  ax-mulcom 11191  ax-addass 11192  ax-mulass 11193  ax-distr 11194  ax-i2m1 11195  ax-1ne0 11196  ax-1rid 11197  ax-rnegex 11198  ax-rrecex 11199  ax-cnre 11200  ax-pre-lttri 11201  ax-pre-lttrn 11202  ax-pre-ltadd 11203

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2100  df-mo 2566  df-eu 2596  df-clab 2741  df-cleq 2754  df-clel 2837  df-nfc 2911  df-ne 2958  df-nel 3064  df-ral 3079  df-rex 3089  df-rab 3415  df-v 3455  df-sbc 3743  df-csb 3851  df-dif 3905  df-un 3907  df-in 3909  df-ss 3919  df-nul 4283  df-if 4486  df-pw 4562  df-sn 4588  df-pr 4590  df-op 4594  df-uni 4871  df-br 5108  df-opab 5172  df-mpt 5191  df-id 5554  df-po 5567  df-so 5568  df-xp 5665  df-rel 5666  df-cnv 5667  df-co 5668  df-dm 5669  df-rn 5670  df-res 5671  df-ima 5672  df-iota 6493  df-fun 6539  df-fn 6540  df-f 6541  df-f1 6542  df-fo 6543  df-f1o 6544  df-fv 6545  df-ov 7419  df-er 8699  df-en 8956  df-dom 8957  df-sdom 8958  df-pnf 11272  df-mnf 11273  df-ltxr 11275

This theorem is used by:  ltaddneg  11453  subsub2  11513  negsub  11533  ltaddpos  11731  addge01  11751  add20  11753  nnge1  12291  nnnn0addcl  12561  un0addcl  12564  uzaddcl  12956  xaddrid  13295  fzosubel3  13784  expadd  14170  faclbnd4lem4  14362  faclbnd6  14365  hashgadd  14443  ccatrid  14655  pfxmpt  14750  pfxfv  14754  pfxswrd  14777  pfxccatin12lem1  14799  pfxccatin12lem2  14802  swrdccat3blem  14810  cshweqrep  14894  relexpaddg  15128  reim0b  15208  rereb  15209  immul2  15226  max0add  15399  iseraltlem2  15772  fsumsplit  15829  sumsplit  15856  binomfallfaclem2  16130  pwp1fsum  16485  bitsinv1lem  16535  sadadd2lem2  16544  sadcaddlem  16551  bezoutlem1  16633  pcadd  16985  pcadd2  16986  pcmpt  16988  vdwapun  17070  vdwlem1  17077  chnccat  18718  mulgnn0dir  19228  psgnunilem2  19623  sylow1lem1  19726  efginvrel2  19855  efgredleme  19871  efgcpbllemb  19883  frgpnabllem1  20001  regsumfsum  21649  pzriprnglem10  21704  regsumsupp  21836  mplcoe5  22257  psdmul  22395  xrsxmet  25037  reparphti  25226  cphpyth  25445  minveclem6  25663  ovolunnul  25729  voliunlem3  25781  ovolioo  25797  itg2splitlem  25977  itg2split  25978  itgrevallem1  26024  itgsplitioo  26067  ditgsplit  26090  dvnadd  26158  dvlipcn  26223  ply1divex  26364  dvntaylp  26604  ulmshft  26623  abelthlem6  26669  cosmpi  26723  sinppi  26724  sinhalfpip  26727  logrnaddcl  26809  affineequiv  27058  chordthmlem3  27069  atanlogaddlem  27148  atanlogsublem  27150  leibpi  27177  scvxcvx  27220  dmgmn0  27260  lgamgulmlem2  27264  lgambdd  27271  logexprlim  27459  2sqblem  27665  2sq2  27667  2sqnn  27673  dchrvmasum2if  27731  dchrvmasumlem  27757  axcontlem8  29414  elntg2  29428  crctcshlem4  30274  eupth2lem3lem6  30699  ipidsq  31177  minvecolem6  31349  normpyc  31613  pjspansn  32044  lnfnmuli  32511  hstoh  32699  indsumin  33294  archirngz  33616  constrrtlc2  34230  constrsslem  34238  2sqr3minply  34277  cos9thpiminply  34285  esumpfinvallem  34571  signsvtp  35078  signlem0  35082  fsum2dsub  35102  cvxpconn  35808  cvxsconn  35809  elmrsubrn  36086  faclim2  36314  fwddifn0  36731  fwddifnp1  36732  dnizeq0  37159  knoppndvlem6  37201  bj-bary1lem  38049  poimirlem1  38357  poimirlem5  38361  poimirlem6  38362  poimirlem7  38363  poimirlem11  38367  poimirlem12  38368  poimirlem17  38373  poimirlem20  38376  poimirlem22  38378  poimirlem24  38380  poimirlem25  38381  poimirlem29  38385  poimirlem31  38387  mblfinlem2  38394  mbfposadd  38403  itg2addnc  38410  itgaddnclem2  38415  ftc1anclem5  38433  ftc1anclem8  38436  areacirc  38449  lcmineqlem4  42885  lcmineqlem18  42899  aks4d1p1p7  42927  aks4d1p3  42931  posbezout  42953  primrootspoweq0  42959  sticksstones10  43008  sticksstones12a  43010  unitscyglem5  43052  3cubeslem2  43517  3cubeslem3r  43519  pell1qrgaplem  43701  jm2.19lem3  43819  jm2.25  43827  relexpaddss  44545  int-add01d  45011  binomcxplemnn0  45160  fperiodmullem  46123  xralrple3  46190  sumnnodd  46447  fprodaddrecnncnvlem  46724  ioodvbdlimc1lem2  46747  volioc  46787  volico  46798  stoweidlem11  46826  stoweidlem26  46841  stirlinglem12  46900  fourierdlem4  46926  fourierdlem42  46964  fourierdlem60  46981  fourierdlem61  46982  fourierdlem92  47013  fourierdlem107  47028  fouriersw  47046  etransclem24  47073  etransclem35  47084  hoidmvlelem2  47411  hspmbllem1  47441  sharhght  47680  deccarry  48186  flmrecm1  48218  nn0mnd  49081  altgsumbcALT  49270  itcovalpclem1  49587  eenglngeehlnmlem2  49655  line2y  49672  itschlc0xyqsol1  49683  itschlc0xyqsol  49684  2itscp  49698  veronesev1lem  50793  veronesev2lem  50794  veronesev3lem  50795  veronesev4lem  50796  veronesev5lem  50797  veronesev6lem  50798