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  9757  exp3vallem  10997  exp3val  10998  exp1  11002  expp1  11003  expcl  11014  expclzaplem  11020  mulexp  11035  sqcl  11057  subsq  11103  subsq2  11104  binom2sub  11110  mulbinom2  11113  binom3  11114  zesq  11116  bernneq  11118  bernneq2  11119  mulsubdivbinom2ap  11170  facnn  11186  fac0  11187  fac1  11188  facp1  11189  bcval5  11222  bcn2  11223  reim  11638  imcl  11640  crre  11643  crim  11644  remim  11646  mulreap  11650  cjreb  11652  recj  11653  reneg  11654  readd  11655  remullem  11657  remul2  11659  imcj  11661  imneg  11662  imadd  11663  immul2  11666  cjadd  11670  ipcnval  11672  cjmulrcl  11673  cjneg  11676  imval2  11680  cjreim  11690  rennim  11789  sqabsadd  11842  sqabssub  11843  absreimsq  11854  absreim  11855  absmul  11856  mul0inf  12031  mulcn2  12102  climmul  12117  isermulc2  12130  fsummulc2  12239  prodf  12329  clim2prod  12330  clim2divap  12331  prod3fmul  12332  prodf1  12333  prodfap0  12336  prodfrecap  12337  prodrbdclem  12362  fproddccvg  12363  prodmodclem3  12366  prodmodclem2a  12367  zproddc  12370  fprodseq  12374  fprodntrivap  12375  prodsnf  12383  fprodcl  12398  fprodclf  12426  efexp  12473  sinf  12495  cosf  12496  tanval2ap  12504  tanval3ap  12505  resinval  12506  recosval  12507  efi4p  12508  resin4p  12509  recos4p  12510  resincl  12511  recoscl  12512  sinneg  12517  cosneg  12518  efival  12523  efmival  12524  efeul  12525  sinadd  12527  cosadd  12528  sinsub  12531  cossub  12532  subsin  12534  sinmul  12535  cosmul  12536  addcos  12537  subcos  12538  cos2tsin  12542  ef01bndlem  12547  sin01bnd  12548  cos01bnd  12549  absef  12561  absefib  12562  efieq1re  12563  demoivre  12564  demoivreALT  12565  odd2np1lem  12663  odd2np1  12664  opoe  12686  omoe  12687  opeo  12688  omeo  12689  modgcd  12792  qredeq  12898  modprm0  13061  pythagtriplem1  13072  pythagtriplem12  13082  pythagtriplem14  13084  gzmulcl  13185  4sqlem11  13208  4sqlem17  13214  cncrng  15014  cnfldmulg  15021  mpomulcn  15809  mulc1cncf  15832  mulcncflem  15850  dvmulxxbr  15945  dvmulxx  15947  dvimulf  15949  plymullem1  15991  plymulcl  15998  plysubcl  15999  efper  16051  sinperlem  16052  sin2kpi  16055  cos2kpi  16056  efimpi  16063  sincosq1eq  16083  abssinper  16090  sinkpi  16091  coskpi  16092  sineq0re  16093  binom4  16236  prmorcht  16299  fsumdvdsmul  16302  ppiqub  16310  bposlem9  16336  lgsdilem2  16377  lgsne0  16379  lgsquadlem1  16418  2sqlem2  16456