Theorem mulcl 8306

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

This proof depends on syntax axioms:   -> wi 4   /\ wa 104   e. wcel 2209  (class class class)co 6085   CCcc 8177   x. cmul 8184

This proof depends on axioms:  ax-mulcl 8277

This theorem is used by:  mpomulf  8316  0cn  8318  mulrid  8323  mulcli  8331  mulcld  8346  mul31  8458  mul4  8459  muladd11r  8483  cnegexlem2  8503  cnegex  8505  muladd  8712  subdi  8713  mul02  8715  submul2  8727  mulsub  8729  recextlem1  8981  recexap  8983  muleqadd  9000  divassap  9022  divmulassap  9027  divmuldivap  9044  divmuleqap  9049  divadddivap  9059  conjmulap  9061  cju  9293  ofnegsub  9294  zneo  9751  exp3vallem  10990  exp3val  10991  exp1  10995  expp1  10996  expcl  11007  expclzaplem  11013  mulexp  11028  sqcl  11050  subsq  11096  subsq2  11097  binom2sub  11103  mulbinom2  11106  binom3  11107  zesq  11109  bernneq  11111  bernneq2  11112  mulsubdivbinom2ap  11163  facnn  11179  fac0  11180  fac1  11181  facp1  11182  bcval5  11215  bcn2  11216  reim  11631  imcl  11633  crre  11636  crim  11637  remim  11639  mulreap  11643  cjreb  11645  recj  11646  reneg  11647  readd  11648  remullem  11650  remul2  11652  imcj  11654  imneg  11655  imadd  11656  immul2  11659  cjadd  11663  ipcnval  11665  cjmulrcl  11666  cjneg  11669  imval2  11673  cjreim  11683  rennim  11782  sqabsadd  11835  sqabssub  11836  absreimsq  11847  absreim  11848  absmul  11849  mul0inf  12023  mulcn2  12094  climmul  12109  isermulc2  12122  fsummulc2  12231  prodf  12321  clim2prod  12322  clim2divap  12323  prod3fmul  12324  prodf1  12325  prodfap0  12328  prodfrecap  12329  prodrbdclem  12354  fproddccvg  12355  prodmodclem3  12358  prodmodclem2a  12359  zproddc  12362  fprodseq  12366  fprodntrivap  12367  prodsnf  12375  fprodcl  12390  fprodclf  12418  efexp  12465  sinf  12487  cosf  12488  tanval2ap  12496  tanval3ap  12497  resinval  12498  recosval  12499  efi4p  12500  resin4p  12501  recos4p  12502  resincl  12503  recoscl  12504  sinneg  12509  cosneg  12510  efival  12515  efmival  12516  efeul  12517  sinadd  12519  cosadd  12520  sinsub  12523  cossub  12524  subsin  12526  sinmul  12527  cosmul  12528  addcos  12529  subcos  12530  cos2tsin  12534  ef01bndlem  12539  sin01bnd  12540  cos01bnd  12541  absef  12553  absefib  12554  efieq1re  12555  demoivre  12556  demoivreALT  12557  odd2np1lem  12655  odd2np1  12656  opoe  12678  omoe  12679  opeo  12680  omeo  12681  modgcd  12784  qredeq  12890  modprm0  13053  pythagtriplem1  13064  pythagtriplem12  13074  pythagtriplem14  13076  gzmulcl  13177  4sqlem11  13200  4sqlem17  13206  cncrng  14955  cnfldmulg  14962  mpomulcn  15716  mulc1cncf  15739  mulcncflem  15757  dvmulxxbr  15852  dvmulxx  15854  dvimulf  15856  plymullem1  15898  plymulcl  15905  plysubcl  15906  efper  15958  sinperlem  15959  sin2kpi  15962  cos2kpi  15963  efimpi  15970  sincosq1eq  15990  abssinper  15997  sinkpi  15998  coskpi  15999  binom4  16138  fsumdvdsmul  16186  ppiqub  16194  lgsdilem2  16253  lgsne0  16255  lgsquadlem1  16294  2sqlem2  16332