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

Theorem mulid2d 9396
Description: Identity law for multiplication. (Contributed by Mario Carneiro, 27-May-2016.)
Hypothesis
Ref Expression
addcld.1  |-  ( ph  ->  A  e.  CC )
Assertion
Ref Expression
mulid2d  |-  ( ph  ->  ( 1  x.  A
)  =  A )

Proof of Theorem mulid2d
StepHypRef Expression
1 addcld.1 . 2  |-  ( ph  ->  A  e.  CC )
2 mulid2 9376 . 2  |-  ( A  e.  CC  ->  (
1  x.  A )  =  A )
31, 2syl 16 1  |-  ( ph  ->  ( 1  x.  A
)  =  A )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    = wceq 1369    e. wcel 1756  (class class class)co 6086   CCcc 9272   1c1 9275    x. cmul 9279
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-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2419  ax-resscn 9331  ax-1cn 9332  ax-icn 9333  ax-addcl 9334  ax-mulcl 9336  ax-mulcom 9338  ax-mulass 9340  ax-distr 9341  ax-1rid 9344  ax-cnre 9347
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 967  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-clab 2425  df-cleq 2431  df-clel 2434  df-nfc 2563  df-ral 2715  df-rex 2716  df-rab 2719  df-v 2969  df-dif 3326  df-un 3328  df-in 3330  df-ss 3337  df-nul 3633  df-if 3787  df-sn 3873  df-pr 3875  df-op 3879  df-uni 4087  df-br 4288  df-iota 5376  df-fv 5421  df-ov 6089
This theorem is referenced by:  addid1  9541  mulcand  9961  receu  9973  divdivdiv  10024  divcan5  10025  subrec  10152  ltrec  10205  recp1lt1  10222  nndivtr  10355  gtndiv  10711  lincmb01cmp  11420  iccf1o  11421  ltdifltdiv  11670  modfrac  11713  modvalp1  11718  m1expcl2  11879  expgt1  11894  ltexp2a  11907  leexp2a  11911  binom3  11977  faclbnd  12058  faclbnd4lem4  12064  facavg  12069  bcval5  12086  cshweqrep  12447  sqrlem2  12725  absimle  12790  reccn2  13066  iseraltlem2  13152  iseraltlem3  13153  o1fsum  13268  abscvgcvg  13274  ackbijnn  13283  binom1p  13286  binom1dif  13288  incexclem  13291  incexc  13292  climcndslem1  13304  geomulcvg  13328  efcllem  13355  ef01bndlem  13460  efieq1re  13475  eirrlem  13478  iddvds  13538  bitsfzolem  13622  bitsfzo  13623  rpmulgcd  13731  prmind2  13766  isprm5  13790  phiprm  13844  eulerthlem2  13849  fermltl  13851  odzdvds  13859  modprm0  13865  pythagtriplem4  13878  pcexp  13918  4sqlem18  14015  vdwapun  14027  mulgnnass  15646  odinv  16053  odadd2  16322  pgpfaclem2  16573  abvneg  16899  nrginvrcnlem  20251  nmoid  20301  blcvx  20355  icopnfcnv  20494  reparphti  20549  pcorevlem  20578  itg11  21149  itg2mulc  21205  itg2monolem1  21208  itgcnlem  21247  iblabs  21286  dvexp  21407  dvef  21432  lhop1lem  21465  dvcvx  21472  dvfsumlem1  21478  dvfsumlem2  21479  dvfsumlem4  21481  dvfsum2  21486  plypow  21653  dgrcolem1  21720  vieta1lem2  21757  radcnvlem1  21858  radcnvlem2  21859  dvradcnv  21866  abelthlem2  21877  abelthlem6  21881  abelthlem7  21883  abelth2  21887  sinhalfpip  21934  sinhalfpim  21935  coshalfpip  21936  coshalfpim  21937  tangtx  21947  efif1olem4  21981  abslogle  22047  logdivlti  22049  advlog  22079  advlogexp  22080  logtayl  22085  cxpaddlelem  22169  cxpaddle  22170  affineequiv  22201  affineequiv2  22202  chordthmlem5  22211  dcubic2  22219  dcubic  22221  mcubic  22222  binom4  22225  dquartlem1  22226  quart1lem  22230  quart1  22231  quartlem1  22232  quart  22236  efiasin  22263  atantayl  22312  cvxcl  22358  scvxcvx  22359  wilthlem1  22386  wilthlem2  22387  basellem9  22406  fsumfldivdiaglem  22509  muinv  22513  chpub  22539  logexprlim  22544  mersenne  22546  perfectlem2  22549  dchrmulid2  22571  dchrptlem1  22583  dchrsum2  22587  sumdchr2  22589  bposlem2  22604  bposlem9  22611  lgsval2lem  22625  lgsval4a  22637  lgsneg1  22639  lgsdir2lem4  22645  lgsdir  22649  lgsdirnn0  22658  lgsdinn0  22659  lgseisenlem1  22668  lgseisenlem2  22669  lgseisenlem4  22671  lgsquad2lem1  22677  2sqlem8  22691  chebbnd1lem3  22700  chpchtlim  22708  rplogsumlem1  22713  rplogsumlem2  22714  rpvmasumlem  22716  dchrmusum2  22723  dchrvmasum2lem  22725  dchrvmasumlem2  22727  dchrvmasumlem3  22728  dchrisum0flblem1  22737  mulog2sumlem2  22764  vmalogdivsum2  22767  2vmadivsumlem  22769  log2sumbnd  22773  selberglem2  22775  chpdifbndlem1  22782  selberg3lem1  22786  selberg4lem1  22789  pntrlog2bndlem2  22807  pntrlog2bndlem5  22810  pntpbnd1  22815  pntpbnd2  22816  pntibndlem2  22820  pntlemb  22826  pntlemr  22831  pntlemk  22835  pntlemo  22836  brbtwn2  23119  colinearalglem4  23123  ax5seglem3  23145  axbtwnid  23153  axpaschlem  23154  axeuclidlem  23176  axcontlem7  23184  axcontlem8  23185  ablomul  23810  mulid  23811  nvm1  24020  nvpi  24022  nvmtri  24027  ipval2  24070  ipasslem1  24199  ipasslem4  24202  bcs2  24552  lnfnaddi  25415  sqsscirc1  26307  indsum  26448  eulerpartlemgs2  26732  plymulx0  26917  lgamgulmlem5  26988  lgamcvg2  27010  lgam1  27019  subfacp1lem6  27042  subfaclim  27045  cvxpcon  27100  cvxscon  27101  rescon  27104  sinccvglem  27286  fprodsplit  27445  fallrisefac  27497  bpolysum  28165  bpolydiflem  28166  bpoly4  28171  mblfinlem3  28401  itg2addnclem3  28416  iblabsnc  28427  iblmulc2nc  28428  ftc1anclem6  28443  ftc1anclem7  28444  ftc1anclem8  28445  areacirclem1  28455  nn0prpwlem  28488  bfplem2  28693  bfp  28694  rrntotbnd  28706  irrapxlem5  29138  pellexlem2  29142  pellexlem6  29146  pellfundex  29198  jm2.19lem3  29311  jm2.25  29319  jm2.27c  29327  jm3.1lem2  29338  flcidc  29502  hashgcdlem  29536  fmul01lt1lem2  29737  itgsinexp  29766  stoweidlem14  29780  stoweidlem26  29792  wallispilem4  29834  wallispilem5  29835  wallispi2lem1  29837  wallispi2  29839  stirlinglem1  29840  stirlinglem3  29842  stirlinglem4  29843  stirlinglem5  29844  stirlinglem6  29845  stirlinglem7  29846  stirlinglem10  29849  mulsubfacd  30143  powm2modprm  30219  ztprmneprm  30709  altgsumbc  30718  bj-bary1lem1  32495
  Copyright terms: Public domain W3C validator