MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  addid1d Structured version   Unicode version

Theorem addid1d 9590
Description:  0 is an additive identity. (Contributed by Mario Carneiro, 27-May-2016.)
Hypothesis
Ref Expression
muld.1  |-  ( ph  ->  A  e.  CC )
Assertion
Ref Expression
addid1d  |-  ( ph  ->  ( A  +  0 )  =  A )

Proof of Theorem addid1d
StepHypRef Expression
1 muld.1 . 2  |-  ( ph  ->  A  e.  CC )
2 addid1 9570 . 2  |-  ( A  e.  CC  ->  ( A  +  0 )  =  A )
31, 2syl 16 1  |-  ( ph  ->  ( A  +  0 )  =  A )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    = wceq 1369    e. wcel 1756  (class class class)co 6112   CCcc 9301   0cc0 9303    + caddc 9306
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-8 1758  ax-9 1760  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2423  ax-sep 4434  ax-nul 4442  ax-pow 4491  ax-pr 4552  ax-un 6393  ax-resscn 9360  ax-1cn 9361  ax-icn 9362  ax-addcl 9363  ax-addrcl 9364  ax-mulcl 9365  ax-mulrcl 9366  ax-mulcom 9367  ax-addass 9368  ax-mulass 9369  ax-distr 9370  ax-i2m1 9371  ax-1ne0 9372  ax-1rid 9373  ax-rnegex 9374  ax-rrecex 9375  ax-cnre 9376  ax-pre-lttri 9377  ax-pre-lttrn 9378  ax-pre-ltadd 9379
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 966  df-3an 967  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-eu 2257  df-mo 2258  df-clab 2430  df-cleq 2436  df-clel 2439  df-nfc 2577  df-ne 2622  df-nel 2623  df-ral 2741  df-rex 2742  df-rab 2745  df-v 2995  df-sbc 3208  df-csb 3310  df-dif 3352  df-un 3354  df-in 3356  df-ss 3363  df-nul 3659  df-if 3813  df-pw 3883  df-sn 3899  df-pr 3901  df-op 3905  df-uni 4113  df-br 4314  df-opab 4372  df-mpt 4373  df-id 4657  df-po 4662  df-so 4663  df-xp 4867  df-rel 4868  df-cnv 4869  df-co 4870  df-dm 4871  df-rn 4872  df-res 4873  df-ima 4874  df-iota 5402  df-fun 5441  df-fn 5442  df-f 5443  df-f1 5444  df-fo 5445  df-f1o 5446  df-fv 5447  df-ov 6115  df-er 7122  df-en 7332  df-dom 7333  df-sdom 7334  df-pnf 9441  df-mnf 9442  df-ltxr 9444
This theorem is referenced by:  subsub2  9658  negsub  9678  ltaddpos  9850  addge01  9870  add20  9872  nnge1  10369  nnnn0addcl  10631  un0addcl  10634  uzaddcl  10932  xaddid1  11230  fzosubel3  11622  expadd  11927  faclbnd4lem4  12093  faclbnd6  12096  hashgadd  12161  ccatrid  12306  lswccat0lsw  12309  swrd0val  12338  swrdid  12342  swrd0fv  12356  swrd0swrd  12376  swrdccatin12lem2b  12398  swrdccatin12lem2  12401  swrdccat3blem  12407  splfv1  12418  cshweqrep  12476  reim0b  12629  rereb  12630  immul2  12647  max0add  12820  iseraltlem2  13181  fsumsplit  13237  sumsplit  13256  bitsinv1lem  13658  sadadd2lem2  13667  sadcaddlem  13674  bezoutlem1  13743  pcadd  13972  pcadd2  13973  pcmpt  13975  vdwapun  14056  vdwlem1  14063  mulgnn0dir  15671  psgnunilem2  16022  sylow1lem1  16118  efginvrel2  16245  efgredleme  16261  efgcpbllemb  16273  frgpnabllem1  16372  mplcoe5  17570  mplcoe2OLD  17572  regsumsupp  18074  xrsxmet  20408  reparphti  20591  minveclem6  20943  ovolunnul  21005  voliunlem3  21055  ovolioo  21071  itg2splitlem  21248  itg2split  21249  itgrevallem1  21294  itgsplitioo  21337  ditgsplit  21358  dvnadd  21425  dvlipcn  21488  ply1divex  21630  dvntaylp  21858  ulmshft  21877  abelthlem6  21923  cosmpi  21972  sinppi  21973  sinhalfpip  21976  logrnaddcl  22048  affineequiv  22243  chordthmlem3  22251  atanlogaddlem  22330  atanlogsublem  22332  leibpi  22359  scvxcvx  22401  logexprlim  22586  2sqblem  22738  dchrvmasum2if  22768  dchrvmasumlem  22794  axcontlem8  23239  eupath2lem3  23622  gxnn0add  23783  ipidsq  24130  minvecolem6  24305  normpyc  24570  pjspansn  25002  lnfnmuli  25470  hstoh  25658  archirngz  26228  regsumfsum  26272  esumpfinvallem  26545  signsvtp  27006  signlem0  27010  dmgmn0  27034  lgamgulmlem2  27038  lgambdd  27045  cvxpcon  27153  cvxscon  27154  binomfallfaclem2  27565  faclim2  27576  mblfinlem2  28455  mbfposadd  28465  itg2addnc  28472  itgaddnclem2  28477  ftc1anclem5  28497  ftc1anclem8  28500  areacirc  28515  pell1qrgaplem  29240  jm2.19lem3  29366  jm2.25  29374  stoweidlem11  29832  stoweidlem26  29847  stirlinglem12  29906  sharhght  29927  altgsumbcALT  30779  bj-bary1lem  32695
  Copyright terms: Public domain W3C validator