Theorem mulcl 8202

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

Syntax hints:   -> wi 4   /\ wa 104   e. wcel 2202  (class class class)co 6028   CCcc 8073   x. cmul 8080

This theorem was proved from axioms:  ax-mulcl 8173

This theorem is referenced by:  mpomulf  8212  0cn  8214  mulrid  8219  mulcli  8227  mulcld  8242  mul31  8352  mul4  8353  muladd11r  8377  cnegexlem2  8397  cnegex  8399  muladd  8605  subdi  8606  mul02  8608  submul2  8620  mulsub  8622  recextlem1  8873  recexap  8875  muleqadd  8890  divassap  8912  divmulassap  8917  divmuldivap  8934  divmuleqap  8939  divadddivap  8949  conjmulap  8951  cju  9183  ofnegsub  9184  zneo  9625  exp3vallem  10848  exp3val  10849  exp1  10853  expp1  10854  expcl  10865  expclzaplem  10871  mulexp  10886  sqcl  10908  subsq  10954  subsq2  10955  binom2sub  10961  mulbinom2  10964  binom3  10965  zesq  10966  bernneq  10968  bernneq2  10969  mulsubdivbinom2ap  11019  facnn  11035  fac0  11036  fac1  11037  facp1  11038  bcval5  11071  bcn2  11072  reim  11475  imcl  11477  crre  11480  crim  11481  remim  11483  mulreap  11487  cjreb  11489  recj  11490  reneg  11491  readd  11492  remullem  11494  remul2  11496  imcj  11498  imneg  11499  imadd  11500  immul2  11503  cjadd  11507  ipcnval  11509  cjmulrcl  11510  cjneg  11513  imval2  11517  cjreim  11526  rennim  11625  sqabsadd  11678  sqabssub  11679  absreimsq  11690  absreim  11691  absmul  11692  mul0inf  11864  mulcn2  11935  climmul  11950  isermulc2  11963  fsummulc2  12072  prodf  12162  clim2prod  12163  clim2divap  12164  prod3fmul  12165  prodf1  12166  prodfap0  12169  prodfrecap  12170  prodrbdclem  12195  fproddccvg  12196  prodmodclem3  12199  prodmodclem2a  12200  zproddc  12203  fprodseq  12207  fprodntrivap  12208  prodsnf  12216  fprodcl  12231  fprodclf  12259  efexp  12306  sinf  12328  cosf  12329  tanval2ap  12337  tanval3ap  12338  resinval  12339  recosval  12340  efi4p  12341  resin4p  12342  recos4p  12343  resincl  12344  recoscl  12345  sinneg  12350  cosneg  12351  efival  12356  efmival  12357  efeul  12358  sinadd  12360  cosadd  12361  sinsub  12364  cossub  12365  subsin  12367  sinmul  12368  cosmul  12369  addcos  12370  subcos  12371  cos2tsin  12375  ef01bndlem  12380  sin01bnd  12381  cos01bnd  12382  absef  12394  absefib  12395  efieq1re  12396  demoivre  12397  demoivreALT  12398  odd2np1lem  12496  odd2np1  12497  opoe  12519  omoe  12520  opeo  12521  omeo  12522  modgcd  12625  qredeq  12731  modprm0  12890  pythagtriplem1  12901  pythagtriplem12  12911  pythagtriplem14  12913  gzmulcl  13014  4sqlem11  13037  4sqlem17  13043  cncrng  14648  cnfldmulg  14655  mpomulcn  15360  mulc1cncf  15383  mulcncflem  15401  dvmulxxbr  15496  dvmulxx  15498  dvimulf  15500  plymullem1  15542  plymulcl  15549  plysubcl  15550  efper  15601  sinperlem  15602  sin2kpi  15605  cos2kpi  15606  efimpi  15613  sincosq1eq  15633  abssinper  15640  sinkpi  15641  coskpi  15642  binom4  15773  fsumdvdsmul  15788  lgsdilem2  15838  lgsne0  15840  lgsquadlem1  15879  2sqlem2  15917