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  8457  mul4  8458  muladd11r  8482  cnegexlem2  8502  cnegex  8504  muladd  8711  subdi  8712  mul02  8714  submul2  8726  mulsub  8728  recextlem1  8979  recexap  8981  muleqadd  8998  divassap  9020  divmulassap  9025  divmuldivap  9042  divmuleqap  9047  divadddivap  9057  conjmulap  9059  cju  9291  ofnegsub  9292  zneo  9747  exp3vallem  10977  exp3val  10978  exp1  10982  expp1  10983  expcl  10994  expclzaplem  11000  mulexp  11015  sqcl  11037  subsq  11083  subsq2  11084  binom2sub  11090  mulbinom2  11093  binom3  11094  zesq  11096  bernneq  11098  bernneq2  11099  mulsubdivbinom2ap  11149  facnn  11165  fac0  11166  fac1  11167  facp1  11168  bcval5  11201  bcn2  11202  reim  11617  imcl  11619  crre  11622  crim  11623  remim  11625  mulreap  11629  cjreb  11631  recj  11632  reneg  11633  readd  11634  remullem  11636  remul2  11638  imcj  11640  imneg  11641  imadd  11642  immul2  11645  cjadd  11649  ipcnval  11651  cjmulrcl  11652  cjneg  11655  imval2  11659  cjreim  11669  rennim  11768  sqabsadd  11821  sqabssub  11822  absreimsq  11833  absreim  11834  absmul  11835  mul0inf  12007  mulcn2  12078  climmul  12093  isermulc2  12106  fsummulc2  12215  prodf  12305  clim2prod  12306  clim2divap  12307  prod3fmul  12308  prodf1  12309  prodfap0  12312  prodfrecap  12313  prodrbdclem  12338  fproddccvg  12339  prodmodclem3  12342  prodmodclem2a  12343  zproddc  12346  fprodseq  12350  fprodntrivap  12351  prodsnf  12359  fprodcl  12374  fprodclf  12402  efexp  12449  sinf  12471  cosf  12472  tanval2ap  12480  tanval3ap  12481  resinval  12482  recosval  12483  efi4p  12484  resin4p  12485  recos4p  12486  resincl  12487  recoscl  12488  sinneg  12493  cosneg  12494  efival  12499  efmival  12500  efeul  12501  sinadd  12503  cosadd  12504  sinsub  12507  cossub  12508  subsin  12510  sinmul  12511  cosmul  12512  addcos  12513  subcos  12514  cos2tsin  12518  ef01bndlem  12523  sin01bnd  12524  cos01bnd  12525  absef  12537  absefib  12538  efieq1re  12539  demoivre  12540  demoivreALT  12541  odd2np1lem  12639  odd2np1  12640  opoe  12662  omoe  12663  opeo  12664  omeo  12665  modgcd  12768  qredeq  12874  modprm0  13033  pythagtriplem1  13044  pythagtriplem12  13054  pythagtriplem14  13056  gzmulcl  13157  4sqlem11  13180  4sqlem17  13186  cncrng  14906  cnfldmulg  14913  mpomulcn  15667  mulc1cncf  15690  mulcncflem  15708  dvmulxxbr  15803  dvmulxx  15805  dvimulf  15807  plymullem1  15849  plymulcl  15856  plysubcl  15857  efper  15908  sinperlem  15909  sin2kpi  15912  cos2kpi  15913  efimpi  15920  sincosq1eq  15940  abssinper  15947  sinkpi  15948  coskpi  15949  binom4  16081  fsumdvdsmul  16105  lgsdilem2  16155  lgsne0  16157  lgsquadlem1  16196  2sqlem2  16234