Theorem mulcl 8296

Description: Alias for ax-mulcl 8267, for naming consistency with mulcli 8321. (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 8267	1 |- ( ( A e. CC /\ B e. CC ) -> ( A x. B ) e. CC )

Syntax hints:   -> wi 4   /\ wa 104   e. wcel 2209  (class class class)co 6075   CCcc 8167   x. cmul 8174

This theorem was proved from axioms:  ax-mulcl 8267

This theorem is referenced by:  mpomulf  8306  0cn  8308  mulrid  8313  mulcli  8321  mulcld  8336  mul31  8447  mul4  8448  muladd11r  8472  cnegexlem2  8492  cnegex  8494  muladd  8701  subdi  8702  mul02  8704  submul2  8716  mulsub  8718  recextlem1  8969  recexap  8971  muleqadd  8988  divassap  9010  divmulassap  9015  divmuldivap  9032  divmuleqap  9037  divadddivap  9047  conjmulap  9049  cju  9281  ofnegsub  9282  zneo  9726  exp3vallem  10955  exp3val  10956  exp1  10960  expp1  10961  expcl  10972  expclzaplem  10978  mulexp  10993  sqcl  11015  subsq  11061  subsq2  11062  binom2sub  11068  mulbinom2  11071  binom3  11072  zesq  11074  bernneq  11076  bernneq2  11077  mulsubdivbinom2ap  11127  facnn  11143  fac0  11144  fac1  11145  facp1  11146  bcval5  11179  bcn2  11180  reim  11595  imcl  11597  crre  11600  crim  11601  remim  11603  mulreap  11607  cjreb  11609  recj  11610  reneg  11611  readd  11612  remullem  11614  remul2  11616  imcj  11618  imneg  11619  imadd  11620  immul2  11623  cjadd  11627  ipcnval  11629  cjmulrcl  11630  cjneg  11633  imval2  11637  cjreim  11647  rennim  11746  sqabsadd  11799  sqabssub  11800  absreimsq  11811  absreim  11812  absmul  11813  mul0inf  11985  mulcn2  12056  climmul  12071  isermulc2  12084  fsummulc2  12193  prodf  12283  clim2prod  12284  clim2divap  12285  prod3fmul  12286  prodf1  12287  prodfap0  12290  prodfrecap  12291  prodrbdclem  12316  fproddccvg  12317  prodmodclem3  12320  prodmodclem2a  12321  zproddc  12324  fprodseq  12328  fprodntrivap  12329  prodsnf  12337  fprodcl  12352  fprodclf  12380  efexp  12427  sinf  12449  cosf  12450  tanval2ap  12458  tanval3ap  12459  resinval  12460  recosval  12461  efi4p  12462  resin4p  12463  recos4p  12464  resincl  12465  recoscl  12466  sinneg  12471  cosneg  12472  efival  12477  efmival  12478  efeul  12479  sinadd  12481  cosadd  12482  sinsub  12485  cossub  12486  subsin  12488  sinmul  12489  cosmul  12490  addcos  12491  subcos  12492  cos2tsin  12496  ef01bndlem  12501  sin01bnd  12502  cos01bnd  12503  absef  12515  absefib  12516  efieq1re  12517  demoivre  12518  demoivreALT  12519  odd2np1lem  12617  odd2np1  12618  opoe  12640  omoe  12641  opeo  12642  omeo  12643  modgcd  12746  qredeq  12852  modprm0  13011  pythagtriplem1  13022  pythagtriplem12  13032  pythagtriplem14  13034  gzmulcl  13135  4sqlem11  13158  4sqlem17  13164  cncrng  14878  cnfldmulg  14885  mpomulcn  15590  mulc1cncf  15613  mulcncflem  15631  dvmulxxbr  15726  dvmulxx  15728  dvimulf  15730  plymullem1  15772  plymulcl  15779  plysubcl  15780  efper  15831  sinperlem  15832  sin2kpi  15835  cos2kpi  15836  efimpi  15843  sincosq1eq  15863  abssinper  15870  sinkpi  15871  coskpi  15872  binom4  16004  fsumdvdsmul  16019  lgsdilem2  16069  lgsne0  16071  lgsquadlem1  16110  2sqlem2  16148