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

Theorem addid2d 9251
Description:  0 is a left identity for addition. (Contributed by Mario Carneiro, 27-May-2016.)
Hypothesis
Ref Expression
muld.1  |-  ( ph  ->  A  e.  CC )
Assertion
Ref Expression
addid2d  |-  ( ph  ->  ( 0  +  A
)  =  A )

Proof of Theorem addid2d
StepHypRef Expression
1 muld.1 . 2  |-  ( ph  ->  A  e.  CC )
2 addid2 9233 . 2  |-  ( A  e.  CC  ->  (
0  +  A )  =  A )
31, 2syl 16 1  |-  ( ph  ->  ( 0  +  A
)  =  A )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1652    e. wcel 1725  (class class class)co 6067   CCcc 8972   0cc0 8974    + caddc 8977
This theorem is referenced by:  negeu  9280  subge0  9525  un0addcl  10237  lincmb01cmp  11022  discr  11499  ccatlid  11731  cats1un  11773  rennim  12027  max0add  12098  fsumsplit  12516  sumsplit  12535  isumsplit  12603  arisum2  12623  efaddlem  12678  eftlub  12693  ef4p  12697  rpnnen2lem11  12807  moddvds  12842  divalglem9  12904  sadadd2lem2  12945  sadcaddlem  12952  pcmpt  13244  4sqlem11  13306  vdwlem6  13337  gsumccat  14770  mulgnn0dir  14896  sylow1lem1  15215  efgsval2  15348  efgsp1  15352  zaddablx  15466  pgpfaclem1  15622  mplcoe2  16513  nrmmetd  18605  blcvx  18812  xrsxmet  18823  reparphti  19005  nulmbl  19413  itg2splitlem  19623  itg2split  19624  itg2monolem1  19625  itgsplitioo  19712  ditgsplit  19731  dvcnp2  19789  dvcmul  19813  dvcmulf  19814  dvmptcmul  19833  dveflem  19846  dvef  19847  dvlipcn  19861  dvlt0  19872  plymullem1  20116  coeeulem  20126  dgradd2  20169  dgrmulc  20172  plydivlem3  20195  aareccl  20226  taylthlem1  20272  sin2kpi  20374  cos2kpi  20375  coshalfpim  20386  sinkpi  20410  chordthmlem3  20658  chordthmlem5  20660  dcubic1lem  20666  dcubic  20669  atancj  20733  atanlogaddlem  20736  atanlogsublem  20738  scvxcvx  20807  ftalem5  20842  ftalem7  20844  basellem3  20848  chtublem  20978  rplogsumlem2  21162  dchrisumlem1  21166  pntrlog2bndlem2  21255  bcm1n  24134  esumpfinvallem  24447  zetacvg  24782  cvxpcon  24912  cvxscon  24913  binomfallfaclem2  25340  brbtwn2  25787  axlowdimlem16  25839  axeuclidlem  25844  mbfposadd  26195  itg2addnc  26200  bfplem2  26464  pellexlem6  26829  jm2.18  26991  stoweidlem1  27659  stoweidlem13  27671  stoweidlem42  27700  stirlinglem5  27736  stirlinglem11  27742  swrdswrd0  28055  swrdccat3b  28073
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-13 1727  ax-14 1729  ax-6 1744  ax-7 1749  ax-11 1761  ax-12 1950  ax-ext 2411  ax-sep 4317  ax-nul 4325  ax-pow 4364  ax-pr 4390  ax-un 4687  ax-resscn 9031  ax-1cn 9032  ax-icn 9033  ax-addcl 9034  ax-addrcl 9035  ax-mulcl 9036  ax-mulrcl 9037  ax-mulcom 9038  ax-addass 9039  ax-mulass 9040  ax-distr 9041  ax-i2m1 9042  ax-1ne0 9043  ax-1rid 9044  ax-rnegex 9045  ax-rrecex 9046  ax-cnre 9047  ax-pre-lttri 9048  ax-pre-lttrn 9049  ax-pre-ltadd 9050
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3or 937  df-3an 938  df-tru 1328  df-ex 1551  df-nf 1554  df-sb 1659  df-eu 2284  df-mo 2285  df-clab 2417  df-cleq 2423  df-clel 2426  df-nfc 2555  df-ne 2595  df-nel 2596  df-ral 2697  df-rex 2698  df-rab 2701  df-v 2945  df-sbc 3149  df-csb 3239  df-dif 3310  df-un 3312  df-in 3314  df-ss 3321  df-nul 3616  df-if 3727  df-pw 3788  df-sn 3807  df-pr 3808  df-op 3810  df-uni 4003  df-br 4200  df-opab 4254  df-mpt 4255  df-id 4485  df-po 4490  df-so 4491  df-xp 4870  df-rel 4871  df-cnv 4872  df-co 4873  df-dm 4874  df-rn 4875  df-res 4876  df-ima 4877  df-iota 5404  df-fun 5442  df-fn 5443  df-f 5444  df-f1 5445  df-fo 5446  df-f1o 5447  df-fv 5448  df-ov 6070  df-er 6891  df-en 7096  df-dom 7097  df-sdom 7098  df-pnf 9106  df-mnf 9107  df-ltxr 9109
  Copyright terms: Public domain W3C validator