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

Theorem addid2d 9562
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 9544 . 2  |-  ( A  e.  CC  ->  (
0  +  A )  =  A )
31, 2syl 16 1  |-  ( ph  ->  ( 0  +  A
)  =  A )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    = wceq 1369    e. wcel 1756  (class class class)co 6086   CCcc 9272   0cc0 9274    + caddc 9277
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 2419  ax-sep 4408  ax-nul 4416  ax-pow 4465  ax-pr 4526  ax-un 6367  ax-resscn 9331  ax-1cn 9332  ax-icn 9333  ax-addcl 9334  ax-addrcl 9335  ax-mulcl 9336  ax-mulrcl 9337  ax-mulcom 9338  ax-addass 9339  ax-mulass 9340  ax-distr 9341  ax-i2m1 9342  ax-1ne0 9343  ax-1rid 9344  ax-rnegex 9345  ax-rrecex 9346  ax-cnre 9347  ax-pre-lttri 9348  ax-pre-lttrn 9349  ax-pre-ltadd 9350
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 2256  df-mo 2257  df-clab 2425  df-cleq 2431  df-clel 2434  df-nfc 2563  df-ne 2603  df-nel 2604  df-ral 2715  df-rex 2716  df-rab 2719  df-v 2969  df-sbc 3182  df-csb 3284  df-dif 3326  df-un 3328  df-in 3330  df-ss 3337  df-nul 3633  df-if 3787  df-pw 3857  df-sn 3873  df-pr 3875  df-op 3879  df-uni 4087  df-br 4288  df-opab 4346  df-mpt 4347  df-id 4631  df-po 4636  df-so 4637  df-xp 4841  df-rel 4842  df-cnv 4843  df-co 4844  df-dm 4845  df-rn 4846  df-res 4847  df-ima 4848  df-iota 5376  df-fun 5415  df-fn 5416  df-f 5417  df-f1 5418  df-fo 5419  df-f1o 5420  df-fv 5421  df-ov 6089  df-er 7093  df-en 7303  df-dom 7304  df-sdom 7305  df-pnf 9412  df-mnf 9413  df-ltxr 9415
This theorem is referenced by:  negeu  9592  subge0  9844  un0addcl  10605  lincmb01cmp  11420  addmodid  11740  discr  11993  ccatlid  12276  swrdspsleq  12334  swrdswrd0  12348  cats1un  12362  swrdccatin2  12370  cshwidx0mod  12433  cshw1  12448  rennim  12720  max0add  12791  fsumsplit  13208  sumsplit  13227  isumsplit  13295  arisum2  13315  efaddlem  13370  eftlub  13385  ef4p  13389  rpnnen2lem11  13499  moddvds  13534  divalglem9  13597  sadadd2lem2  13638  sadcaddlem  13645  pcmpt  13946  4sqlem11  14008  vdwlem6  14039  gsumccat  15510  mulgnn0dir  15641  sylow1lem1  16088  efgsval2  16221  efgsp1  16225  zaddablx  16341  pgpfaclem1  16572  mplcoe5  17528  mplcoe2OLD  17530  regsumsupp  18032  nrmmetd  20147  blcvx  20355  xrsxmet  20366  reparphti  20549  nulmbl  20997  itg2splitlem  21206  itg2split  21207  itg2monolem1  21208  itgsplitioo  21295  ditgsplit  21316  dvcnp2  21374  dvcmul  21398  dvcmulf  21399  dvmptcmul  21418  dveflem  21431  dvef  21432  dvlipcn  21446  dvlt0  21457  plymullem1  21662  coeeulem  21672  dgradd2  21715  dgrmulc  21718  plydivlem3  21741  aareccl  21772  taylthlem1  21818  sin2kpi  21925  cos2kpi  21926  coshalfpim  21937  sinkpi  21961  chordthmlem3  22209  chordthmlem5  22211  dcubic1lem  22218  dcubic  22221  atancj  22285  atanlogaddlem  22288  atanlogsublem  22290  scvxcvx  22359  ftalem5  22394  ftalem7  22396  basellem3  22400  chtublem  22530  rplogsumlem2  22714  dchrisumlem1  22718  pntrlog2bndlem2  22807  brbtwn2  23119  axlowdimlem16  23171  axeuclidlem  23176  bcm1n  26047  regsumfsum  26218  esumpfinvallem  26492  signsplypnf  26920  signstfvn  26939  zetacvg  26970  cvxpcon  27100  cvxscon  27101  binomfallfaclem2  27512  tan2h  28395  mbfposadd  28410  itg2addnc  28417  ftc1anclem5  28442  bfplem2  28693  pellexlem6  29146  jm2.18  29308  stoweidlem1  29767  stoweidlem13  29779  stoweidlem42  29808  stirlinglem5  29844  stirlinglem11  29850  cnambpcma  30139  altgsumbcALT  30719  bj-flbi3  32427
  Copyright terms: Public domain W3C validator