Theorem addridd 11481

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 11461	. 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 7408  ℂcc 11169  0cc0 11171   + caddc 11174

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 2213  ax-ext 2732  ax-sep 5248  ax-nul 5259  ax-pow 5326  ax-pr 5390  ax-un 7734  ax-resscn 11228  ax-1cn 11229  ax-icn 11230  ax-addcl 11231  ax-addrcl 11232  ax-mulcl 11233  ax-mulrcl 11234  ax-mulcom 11235  ax-addass 11236  ax-mulass 11237  ax-distr 11238  ax-i2m1 11239  ax-1ne0 11240  ax-1rid 11241  ax-rnegex 11242  ax-rrecex 11243  ax-cnre 11244  ax-pre-lttri 11245  ax-pre-lttrn 11246  ax-pre-ltadd 11247

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 2564  df-eu 2594  df-clab 2739  df-cleq 2752  df-clel 2835  df-nfc 2909  df-ne 2956  df-nel 3062  df-ral 3077  df-rex 3087  df-rab 3413  df-v 3452  df-sbc 3739  df-csb 3847  df-dif 3901  df-un 3903  df-in 3905  df-ss 3915  df-nul 4279  df-if 4482  df-pw 4558  df-sn 4584  df-pr 4586  df-op 4590  df-uni 4867  df-br 5103  df-opab 5167  df-mpt 5186  df-id 5542  df-po 5555  df-so 5556  df-xp 5653  df-rel 5654  df-cnv 5655  df-co 5656  df-dm 5657  df-rn 5658  df-res 5659  df-ima 5660  df-iota 6483  df-fun 6529  df-fn 6530  df-f 6531  df-f1 6532  df-fo 6533  df-f1o 6534  df-fv 6535  df-ov 7411  df-er 8695  df-en 8952  df-dom 8953  df-sdom 8954  df-pnf 11316  df-mnf 11317  df-ltxr 11319

This theorem is used by:  ltaddneg  11497  subsub2  11557  negsub  11577  ltaddpos  11775  addge01  11795  add20  11797  nnge1  12335  nnnn0addcl  12605  un0addcl  12608  uzaddcl  13000  xaddrid  13340  fzosubel3  13829  expadd  14215  faclbnd4lem4  14407  faclbnd6  14410  hashgadd  14488  ccatrid  14700  pfxmpt  14795  pfxfv  14799  pfxswrd  14822  pfxccatin12lem1  14844  pfxccatin12lem2  14847  swrdccat3blem  14855  cshweqrep  14939  relexpaddg  15173  reim0b  15253  rereb  15254  immul2  15271  max0add  15444  iseraltlem2  15817  fsumsplit  15874  sumsplit  15901  binomfallfaclem2  16173  pwp1fsum  16528  bitsinv1lem  16578  sadadd2lem2  16587  sadcaddlem  16594  bezoutlem1  16676  pcadd  17028  pcadd2  17029  pcmpt  17031  vdwapun  17113  vdwlem1  17120  chnccat  18761  mulgnn0dir  19275  psgnunilem2  19670  sylow1lem1  19773  efginvrel2  19902  efgredleme  19918  efgcpbllemb  19930  frgpnabllem1  20048  regsumfsum  21702  pzriprnglem10  21757  regsumsupp  21889  mplcoe5  22310  psdmul  22448  xrsxmet  25090  reparphti  25279  cphpyth  25498  minveclem6  25716  ovolunnul  25782  voliunlem3  25834  ovolioo  25850  itg2splitlem  26030  itg2split  26031  itgrevallem1  26076  itgsplitioo  26119  ditgsplit  26142  dvnadd  26210  dvlipcn  26275  ply1divex  26416  dvntaylp  26661  ulmshft  26680  abelthlem6  26726  cosmpi  26780  sinppi  26781  sinhalfpip  26784  logrnaddcl  26865  affineequiv  27114  chordthmlem3  27125  atanlogaddlem  27204  atanlogsublem  27206  leibpi  27233  scvxcvx  27276  dmgmn0  27316  lgamgulmlem2  27320  lgambdd  27327  logexprlim  27515  2sqblem  27721  2sq2  27723  2sqnn  27729  dchrvmasum2if  27787  dchrvmasumlem  27813  axcontlem8  29482  elntg2  29496  crctcshlem4  30342  eupth2lem3lem6  30767  ipidsq  31245  minvecolem6  31417  normpyc  31681  pjspansn  32112  lnfnmuli  32579  hstoh  32767  indsumin  33361  archirngz  33683  constrrtlc2  34298  constrsslem  34306  2sqr3minply  34345  cos9thpiminply  34353  esumpfinvallem  34639  signsvtp  35146  signlem0  35150  fsum2dsub  35170  cvxpconn  35928  cvxsconn  35929  elmrsubrn  36206  faclim2  36434  fwddifn0  36851  fwddifnp1  36852  dnizeq0  37263  knoppndvlem6  37305  bj-bary1lem  38151  poimirlem1  38459  poimirlem5  38463  poimirlem6  38464  poimirlem7  38465  poimirlem11  38469  poimirlem12  38470  poimirlem17  38475  poimirlem20  38478  poimirlem22  38480  poimirlem24  38482  poimirlem25  38483  poimirlem29  38487  poimirlem31  38489  mblfinlem2  38496  mbfposadd  38505  itg2addnc  38512  itgaddnclem2  38517  ftc1anclem5  38535  ftc1anclem8  38538  areacirc  38551  lcmineqlem4  43002  lcmineqlem18  43016  aks4d1p1p7  43044  aks4d1p3  43048  posbezout  43070  primrootspoweq0  43076  sticksstones10  43125  sticksstones12a  43127  unitscyglem5  43169  3cubeslem2  43634  3cubeslem3r  43636  pell1qrgaplem  43818  jm2.19lem3  43936  jm2.25  43944  relexpaddss  44662  int-add01d  45128  binomcxplemnn0  45277  fperiodmullem  46240  xralrple3  46307  sumnnodd  46564  fprodaddrecnncnvlem  46841  ioodvbdlimc1lem2  46864  volioc  46904  volico  46915  stoweidlem11  46943  stoweidlem26  46958  stirlinglem12  47017  fourierdlem4  47043  fourierdlem42  47081  fourierdlem60  47098  fourierdlem61  47099  fourierdlem92  47130  fourierdlem107  47145  fouriersw  47163  etransclem24  47190  etransclem35  47201  hoidmvlelem2  47528  hspmbllem1  47558  sharhght  47797  deccarry  48303  flmrecm1  48335  nn0mnd  49198  altgsumbcALT  49387  itcovalpclem1  49704  eenglngeehlnmlem2  49772  line2y  49789  itschlc0xyqsol1  49800  itschlc0xyqsol  49801  2itscp  49815  veronesev1lem  50895  veronesev2lem  50896  veronesev3lem  50897  veronesev4lem  50898  veronesev5lem  50899  veronesev6lem  50900