Theorem mulcl 9378

Description: Alias for ax-mulcl 9356, for naming consistency with mulcli 9403. (Contributed by NM, 10-Mar-2008.)

Assertion

Ref	Expression
mulcl	|- ( ( A e. CC /\ B e. CC ) -> ( A x. B ) e. CC )

Proof of Theorem mulcl

Step	Hyp	Ref	Expression
1		ax-mulcl 9356	1 |- ( ( A e. CC /\ B e. CC ) -> ( A x. B ) e. CC )

Syntax hints:   -> wi 4   /\ wa 369   e. wcel 1756  (class class class)co 6103   CCcc 9292   x. cmul 9299

This theorem was proved from axioms:  ax-mulcl 9356

This theorem is referenced by:  0cn  9390  mulid1  9395  mulcli  9403  mulcld  9418  mul31  9549  mul4  9550  mul02  9559  cnegex2  9563  muladd  9789  subdi  9790  submul2  9797  mulsub  9799  recextlem1  9978  recex  9980  muleqadd  9992  mulnzcnopr  9994  mulcan1g  10001  divass  10024  divmuldiv  10043  divmuleq  10048  divadddiv  10058  conjmul  10060  cju  10330  zneo  10736  cnref1o  10998  modcyc2  11756  modaddmulmod  11777  expcl  11895  expclzlem  11901  mulexp  11915  sqcl  11940  subsq  11985  subsq2  11986  binom2sub  11995  binom3  11997  zesq  11999  bernneq  12002  bernneq2  12003  bcval5  12106  reim  12610  imcl  12612  crre  12615  crim  12616  remim  12618  mulre  12622  cjreb  12624  recj  12625  reneg  12626  readd  12627  remullem  12629  remul2  12631  imcj  12633  imneg  12634  imadd  12635  immul2  12638  cjadd  12642  ipcnval  12644  cjmulrcl  12645  cjneg  12648  imval2  12652  cjreim  12661  rennim  12740  cnpart  12741  sqrneg  12769  sqabsadd  12783  sqabssub  12784  absreimsq  12793  absreim  12794  absmul  12795  sqreulem  12859  sqreu  12860  mulcn2  13085  o1mul  13104  climmul  13122  iseraltlem2  13172  efexp  13397  sinf  13420  cosf  13421  tanval2  13429  tanval3  13430  resinval  13431  recosval  13432  efi4p  13433  resin4p  13434  recos4p  13435  resincl  13436  recoscl  13437  sinneg  13442  cosneg  13443  efival  13448  efmival  13449  sinhval  13450  coshval  13451  retanhcl  13455  tanhlt1  13456  tanhbnd  13457  efeul  13458  sinadd  13460  cosadd  13461  sinsub  13464  cossub  13465  subsin  13467  sinmul  13468  cosmul  13469  addcos  13470  subcos  13471  cos2tsin  13475  ef01bndlem  13480  sin01bnd  13481  cos01bnd  13482  absef  13493  absefib  13494  efieq1re  13495  demoivre  13496  demoivreALT  13497  dvdscmulr  13573  dvdsmulcr  13574  odd2np1lem  13603  odd2np1  13604  gcdaddm  13725  modgcd  13732  bezoutlem1  13734  qredeq  13804  eulerthlem2  13869  modprm0  13885  opoe  13890  omoe  13891  opeo  13892  omeo  13893  pythagtriplem1  13895  pythagtriplem12  13905  pythagtriplem14  13907  iserodd  13914  gzmulcl  14011  4sqlem11  14028  4sqlem17  14034  cncrng  17849  cnfldmulg  17860  cnsubrg  17885  mulc1cncf  20493  icccvx  20534  pcorevlem  20610  itgcnlem  21279  itgneg  21293  itgconst  21308  itgadd  21314  iblabs  21318  itgmulc2  21323  dvmulbr  21425  dvmulf  21429  dvsincos  21465  plymullem1  21694  plymulcl  21701  plysubcl  21702  dgrcolem1  21752  dgrcolem2  21753  plydivlem4  21774  quotlem  21778  quotcl2  21780  quotdgr  21781  aaliou3lem3  21822  efper  21953  sinperlem  21954  sin2kpi  21957  cos2kpi  21958  efimpi  21965  sincosq1eq  21986  pige3  21991  abssinper  21992  sinkpi  21993  coskpi  21994  sineq0  21995  coseq1  21996  tanregt0  22007  efgh  22009  efif1olem4  22013  efifo  22015  eff1olem  22016  lognegb  22050  eflogeq  22062  efiarg  22068  tanarg  22080  logf1o2  22107  cxpcl  22131  cxpne0  22134  cxpsqrlem  22159  cxpsqr  22160  dvcxp1  22192  root1eq1  22205  cxpeq  22207  quad2  22246  quad  22247  dcubic2  22251  dcubic1  22252  dcubic  22253  mcubic  22254  cubic2  22255  cubic  22256  binom4  22257  dquartlem1  22258  dquartlem2  22259  dquart  22260  quart1cl  22261  quart1lem  22262  quart1  22263  quartlem1  22264  quartlem2  22265  quartlem3  22266  quart  22268  asinlem  22275  asinlem2  22276  asinlem3a  22277  asinlem3  22278  asinf  22279  atandm2  22284  atanf  22287  asinneg  22293  efiasin  22295  sinasin  22296  asinsinlem  22298  asinsin  22299  asinbnd  22306  cosasin  22311  atanneg  22314  atancj  22317  efiatan  22319  atanlogaddlem  22320  atanlogadd  22321  atanlogsublem  22322  atanlogsub  22323  efiatan2  22324  2efiatan  22325  tanatan  22326  cosatan  22328  atantan  22330  atanbndlem  22332  atans2  22338  dvatan  22342  atantayl  22344  atantayl2  22345  leibpilem1  22347  leibpilem2  22348  efrlim  22375  ftalem7  22428  basellem3  22432  basellem7  22436  basellem8  22437  basellem9  22438  ppiub  22555  dchrmulcl  22600  bposlem9  22643  lgsdir  22681  lgsdilem2  22682  lgsdi  22683  lgsne0  22684  lgsquadlem1  22705  2sqlem2  22715  rpvmasum2  22773  dchrisum0lem1  22777  dchrisum0lem2  22779  mulogsumlem  22792  mulog2sumlem3  22797  log2sumbnd  22805  selberglem1  22806  selberglem2  22807  selberg2  22812  pntlemk  22867  colinearalglem1  23164  colinearalglem2  23165  ax5seglem1  23186  axcontlem2  23223  axcontlem8  23229  ablomul  23854  efghgrp  23872  smcnlem  24104  ipval2  24114  4ipval2  24115  4ipval3  24119  ipidsq  24120  dipcj  24124  cncph  24231  ipasslem2  24244  ipasslem4  24246  ipasslem9  24250  ipasslem11  24252  hhssnv  24677  spansncol  24983  homulass  25218  lnfnmuli  25460  riesz3i  25478  zetacvg  27013  circum  27331  prodf  27414  clim2div  27416  prodfmul  27417  prodfn0  27421  prodfrec  27422  prodfdiv  27423  prodmolem3  27458  prodmolem2a  27459  fprodcl  27477  risefaccl  27530  fallfaccl  27531  faclim  27564  bpoly3  28213  fsumcube  28215  sin2h  28434  cos2h  28435  dvtanlem  28453  itg2addnclem3  28457  itgaddnc  28464  iblabsnc  28468  iblmulc2nc  28469  itgmulc2nc  28472  ftc1anclem3  28481  ftc1anclem6  28484  ftc1anclem7  28485  ftc1anclem8  28486  ftc1anc  28487  dvcncxp1  28489  dvasin  28492  cntotbnd  28707  rmxluc  29289  rmyluc  29290  jm2.17a  29315  jm2.18  29349  jm3.1lem1  29378  jm3.1lem2  29379  proot1ex  29581  lhe4.4ex1a  29615  expgrowthi  29619  expgrowth  29621  stoweidlem10  29817  wallispi2lem1  29878  wallispi2  29880  numclwlk3lem3  30678  sinh-conventional  31086  dpfrac1  31119