Theorem mulcl 8312

Description: Alias for ax-mulcl 8283, for naming consistency with mulcli 8337. (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 8283	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 6088   CCcc 8183   x. cmul 8190

This proof depends on axioms:  ax-mulcl 8283

This theorem is used by:  mpomulf  8322  0cn  8324  mulrid  8329  mulcli  8337  mulcld  8352  mul31  8464  mul4  8465  muladd11r  8489  cnegexlem2  8509  cnegex  8511  muladd  8718  subdi  8719  mul02  8721  submul2  8733  mulsub  8735  recextlem1  8987  recexap  8989  muleqadd  9006  divassap  9028  divmulassap  9033  divmuldivap  9050  divmuleqap  9055  divadddivap  9065  conjmulap  9067  cju  9299  ofnegsub  9301  zneo  9758  exp3vallem  10998  exp3val  10999  exp1  11003  expp1  11004  expcl  11015  expclzaplem  11021  mulexp  11036  sqcl  11058  subsq  11104  subsq2  11105  binom2sub  11111  mulbinom2  11114  binom3  11115  zesq  11117  bernneq  11119  bernneq2  11120  mulsubdivbinom2ap  11171  facnn  11187  fac0  11188  fac1  11189  facp1  11190  bcval5  11223  bcn2  11224  reim  11639  imcl  11641  crre  11644  crim  11645  remim  11647  mulreap  11651  cjreb  11653  recj  11654  reneg  11655  readd  11656  remullem  11658  remul2  11660  imcj  11662  imneg  11663  imadd  11664  immul2  11667  cjadd  11671  ipcnval  11673  cjmulrcl  11674  cjneg  11677  imval2  11681  cjreim  11691  rennim  11790  sqabsadd  11843  sqabssub  11844  absreimsq  11855  absreim  11856  absmul  11857  mul0inf  12032  mulcn2  12103  climmul  12118  isermulc2  12131  fsummulc2  12240  prodf  12330  clim2prod  12331  clim2divap  12332  prod3fmul  12333  prodf1  12334  prodfap0  12337  prodfrecap  12338  prodrbdclem  12363  fproddccvg  12364  prodmodclem3  12367  prodmodclem2a  12368  zproddc  12371  fprodseq  12375  fprodntrivap  12376  prodsnf  12384  fprodcl  12399  fprodclf  12427  efexp  12474  sinf  12496  cosf  12497  tanval2ap  12505  tanval3ap  12506  resinval  12507  recosval  12508  efi4p  12509  resin4p  12510  recos4p  12511  resincl  12512  recoscl  12513  sinneg  12518  cosneg  12519  efival  12524  efmival  12525  efeul  12526  sinadd  12528  cosadd  12529  sinsub  12532  cossub  12533  subsin  12535  sinmul  12536  cosmul  12537  addcos  12538  subcos  12539  cos2tsin  12543  ef01bndlem  12548  sin01bnd  12549  cos01bnd  12550  absef  12562  absefib  12563  efieq1re  12564  demoivre  12565  demoivreALT  12566  odd2np1lem  12664  odd2np1  12665  opoe  12687  omoe  12688  opeo  12689  omeo  12690  modgcd  12793  qredeq  12899  modprm0  13062  pythagtriplem1  13073  pythagtriplem12  13083  pythagtriplem14  13085  gzmulcl  13186  4sqlem11  13209  4sqlem17  13215  cncrng  15015  cnfldmulg  15022  mpomulcn  15792  mulc1cncf  15815  mulcncflem  15833  dvmulxxbr  15928  dvmulxx  15930  dvimulf  15932  plymullem1  15974  plymulcl  15981  plysubcl  15982  efper  16034  sinperlem  16035  sin2kpi  16038  cos2kpi  16039  efimpi  16046  sincosq1eq  16066  abssinper  16073  sinkpi  16074  coskpi  16075  sineq0re  16076  binom4  16219  prmorcht  16282  fsumdvdsmul  16285  ppiqub  16293  bposlem9  16319  lgsdilem2  16360  lgsne0  16362  lgsquadlem1  16401  2sqlem2  16439