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

Theorem addid1d 9230
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 9210 . 2  |-  ( A  e.  CC  ->  ( A  +  0 )  =  A )
31, 2syl 16 1  |-  ( ph  ->  ( A  +  0 )  =  A )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1649    e. wcel 1721  (class class class)co 6048   CCcc 8952   0cc0 8954    + caddc 8957
This theorem is referenced by:  subsub2  9293  negsub  9313  ltaddpos  9482  addge01  9502  add20  9504  nnge1  9990  nnnn0addcl  10215  un0addcl  10217  uzaddcl  10497  xaddid1  10789  fzosubel3  11142  expadd  11385  faclbnd4lem4  11550  faclbnd6  11553  hashgadd  11614  ccatrid  11712  swrd0val  11731  swrdid  11735  splfv1  11747  reim0b  11887  rereb  11888  immul2  11905  max0add  12078  iseraltlem2  12439  fsumsplit  12496  sumsplit  12515  bitsinv1lem  12916  sadadd2lem2  12925  sadcaddlem  12932  bezoutlem1  13001  pcadd  13221  pcadd2  13222  pcmpt  13224  vdwapun  13305  vdwlem1  13312  mulgnn0dir  14876  sylow1lem1  15195  efginvrel2  15322  efgredleme  15338  efgcpbllemb  15350  frgpnabllem1  15447  mplcoe2  16493  xrsxmet  18801  reparphti  18983  minveclem6  19296  ovolunnul  19357  voliunlem3  19407  ovolioo  19423  itg2splitlem  19601  itg2split  19602  itgrevallem1  19647  itgsplitioo  19690  ditgsplit  19709  dvnadd  19776  dvlipcn  19839  ply1divex  20020  dvntaylp  20248  ulmshft  20267  abelthlem6  20313  cosmpi  20357  sinppi  20358  sinhalfpip  20361  logrnaddcl  20433  affineequiv  20628  chordthmlem3  20636  atanlogaddlem  20714  atanlogsublem  20716  leibpi  20743  scvxcvx  20785  logexprlim  20970  2sqblem  21122  dchrvmasum2if  21152  dchrvmasumlem  21178  eupath2lem3  21662  gxnn0add  21823  ipidsq  22170  minvecolem6  22345  normpyc  22609  pjspansn  23040  lnfnmuli  23508  hstoh  23696  esumpfinvallem  24425  dmgmn0  24771  lgamgulmlem2  24775  lgambdd  24782  cvxpcon  24890  cvxscon  24891  binomfallfaclem2  25315  faclim2  25323  axcontlem8  25822  mblfinlem  26151  mbfposadd  26161  itg2addnc  26166  itgaddnclem2  26171  areacirc  26195  pell1qrgaplem  26834  jm2.19lem3  26960  jm2.25  26968  psgnunilem2  27294  stoweidlem11  27635  stoweidlem26  27650  stirlinglem12  27709  sharhght  27730  ubmelfzo  27994  swrdccatin12lem3b  28030  swrdccatin12lem3  28032  swrdccat3b  28039
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-13 1723  ax-14 1725  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2393  ax-sep 4298  ax-nul 4306  ax-pow 4345  ax-pr 4371  ax-un 4668  ax-resscn 9011  ax-1cn 9012  ax-icn 9013  ax-addcl 9014  ax-addrcl 9015  ax-mulcl 9016  ax-mulrcl 9017  ax-mulcom 9018  ax-addass 9019  ax-mulass 9020  ax-distr 9021  ax-i2m1 9022  ax-1ne0 9023  ax-1rid 9024  ax-rnegex 9025  ax-rrecex 9026  ax-cnre 9027  ax-pre-lttri 9028  ax-pre-lttrn 9029  ax-pre-ltadd 9030
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3or 937  df-3an 938  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-eu 2266  df-mo 2267  df-clab 2399  df-cleq 2405  df-clel 2408  df-nfc 2537  df-ne 2577  df-nel 2578  df-ral 2679  df-rex 2680  df-rab 2683  df-v 2926  df-sbc 3130  df-csb 3220  df-dif 3291  df-un 3293  df-in 3295  df-ss 3302  df-nul 3597  df-if 3708  df-pw 3769  df-sn 3788  df-pr 3789  df-op 3791  df-uni 3984  df-br 4181  df-opab 4235  df-mpt 4236  df-id 4466  df-po 4471  df-so 4472  df-xp 4851  df-rel 4852  df-cnv 4853  df-co 4854  df-dm 4855  df-rn 4856  df-res 4857  df-ima 4858  df-iota 5385  df-fun 5423  df-fn 5424  df-f 5425  df-f1 5426  df-fo 5427  df-f1o 5428  df-fv 5429  df-ov 6051  df-er 6872  df-en 7077  df-dom 7078  df-sdom 7079  df-pnf 9086  df-mnf 9087  df-ltxr 9089
  Copyright terms: Public domain W3C validator