Theorem mulcl 8307

Description: Alias for ax-mulcl 8278, for naming consistency with mulcli 8332. (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 8278	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 8178   x. cmul 8185

This proof depends on axioms:  ax-mulcl 8278

This theorem is used by:  mpomulf  8317  0cn  8319  mulrid  8324  mulcli  8332  mulcld  8347  mul31  8459  mul4  8460  muladd11r  8484  cnegexlem2  8504  cnegex  8506  muladd  8713  subdi  8714  mul02  8716  submul2  8728  mulsub  8730  recextlem1  8982  recexap  8984  muleqadd  9001  divassap  9023  divmulassap  9028  divmuldivap  9045  divmuleqap  9050  divadddivap  9060  conjmulap  9062  cju  9294  ofnegsub  9295  zneo  9752  exp3vallem  10992  exp3val  10993  exp1  10997  expp1  10998  expcl  11009  expclzaplem  11015  mulexp  11030  sqcl  11052  subsq  11098  subsq2  11099  binom2sub  11105  mulbinom2  11108  binom3  11109  zesq  11111  bernneq  11113  bernneq2  11114  mulsubdivbinom2ap  11165  facnn  11181  fac0  11182  fac1  11183  facp1  11184  bcval5  11217  bcn2  11218  reim  11633  imcl  11635  crre  11638  crim  11639  remim  11641  mulreap  11645  cjreb  11647  recj  11648  reneg  11649  readd  11650  remullem  11652  remul2  11654  imcj  11656  imneg  11657  imadd  11658  immul2  11661  cjadd  11665  ipcnval  11667  cjmulrcl  11668  cjneg  11671  imval2  11675  cjreim  11685  rennim  11784  sqabsadd  11837  sqabssub  11838  absreimsq  11849  absreim  11850  absmul  11851  mul0inf  12026  mulcn2  12097  climmul  12112  isermulc2  12125  fsummulc2  12234  prodf  12324  clim2prod  12325  clim2divap  12326  prod3fmul  12327  prodf1  12328  prodfap0  12331  prodfrecap  12332  prodrbdclem  12357  fproddccvg  12358  prodmodclem3  12361  prodmodclem2a  12362  zproddc  12365  fprodseq  12369  fprodntrivap  12370  prodsnf  12378  fprodcl  12393  fprodclf  12421  efexp  12468  sinf  12490  cosf  12491  tanval2ap  12499  tanval3ap  12500  resinval  12501  recosval  12502  efi4p  12503  resin4p  12504  recos4p  12505  resincl  12506  recoscl  12507  sinneg  12512  cosneg  12513  efival  12518  efmival  12519  efeul  12520  sinadd  12522  cosadd  12523  sinsub  12526  cossub  12527  subsin  12529  sinmul  12530  cosmul  12531  addcos  12532  subcos  12533  cos2tsin  12537  ef01bndlem  12542  sin01bnd  12543  cos01bnd  12544  absef  12556  absefib  12557  efieq1re  12558  demoivre  12559  demoivreALT  12560  odd2np1lem  12658  odd2np1  12659  opoe  12681  omoe  12682  opeo  12683  omeo  12684  modgcd  12787  qredeq  12893  modprm0  13056  pythagtriplem1  13067  pythagtriplem12  13077  pythagtriplem14  13079  gzmulcl  13180  4sqlem11  13203  4sqlem17  13209  cncrng  14990  cnfldmulg  14997  mpomulcn  15758  mulc1cncf  15781  mulcncflem  15799  dvmulxxbr  15894  dvmulxx  15896  dvimulf  15898  plymullem1  15940  plymulcl  15947  plysubcl  15948  efper  16000  sinperlem  16001  sin2kpi  16004  cos2kpi  16005  efimpi  16012  sincosq1eq  16032  abssinper  16039  sinkpi  16040  coskpi  16041  binom4  16180  prmorcht  16243  fsumdvdsmul  16246  ppiqub  16254  bposlem9  16280  lgsdilem2  16321  lgsne0  16323  lgsquadlem1  16362  2sqlem2  16400