Theorem mulcl 8122

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

Syntax hints:   -> wi 4   /\ wa 104   e. wcel 2200  (class class class)co 6000   CCcc 7993   x. cmul 8000

This theorem was proved from axioms:  ax-mulcl 8093

This theorem is referenced by:  mpomulf  8132  0cn  8134  mulrid  8139  mulcli  8147  mulcld  8163  mul31  8273  mul4  8274  muladd11r  8298  cnegexlem2  8318  cnegex  8320  muladd  8526  subdi  8527  mul02  8529  submul2  8541  mulsub  8543  recextlem1  8794  recexap  8796  muleqadd  8811  divassap  8833  divmulassap  8838  divmuldivap  8855  divmuleqap  8860  divadddivap  8870  conjmulap  8872  cju  9104  ofnegsub  9105  zneo  9544  exp3vallem  10757  exp3val  10758  exp1  10762  expp1  10763  expcl  10774  expclzaplem  10780  mulexp  10795  sqcl  10817  subsq  10863  subsq2  10864  binom2sub  10870  mulbinom2  10873  binom3  10874  zesq  10875  bernneq  10877  bernneq2  10878  mulsubdivbinom2ap  10928  facnn  10944  fac0  10945  fac1  10946  facp1  10947  bcval5  10980  bcn2  10981  reim  11358  imcl  11360  crre  11363  crim  11364  remim  11366  mulreap  11370  cjreb  11372  recj  11373  reneg  11374  readd  11375  remullem  11377  remul2  11379  imcj  11381  imneg  11382  imadd  11383  immul2  11386  cjadd  11390  ipcnval  11392  cjmulrcl  11393  cjneg  11396  imval2  11400  cjreim  11409  rennim  11508  sqabsadd  11561  sqabssub  11562  absreimsq  11573  absreim  11574  absmul  11575  mul0inf  11747  mulcn2  11818  climmul  11833  isermulc2  11846  fsummulc2  11954  prodf  12044  clim2prod  12045  clim2divap  12046  prod3fmul  12047  prodf1  12048  prodfap0  12051  prodfrecap  12052  prodrbdclem  12077  fproddccvg  12078  prodmodclem3  12081  prodmodclem2a  12082  zproddc  12085  fprodseq  12089  fprodntrivap  12090  prodsnf  12098  fprodcl  12113  fprodclf  12141  efexp  12188  sinf  12210  cosf  12211  tanval2ap  12219  tanval3ap  12220  resinval  12221  recosval  12222  efi4p  12223  resin4p  12224  recos4p  12225  resincl  12226  recoscl  12227  sinneg  12232  cosneg  12233  efival  12238  efmival  12239  efeul  12240  sinadd  12242  cosadd  12243  sinsub  12246  cossub  12247  subsin  12249  sinmul  12250  cosmul  12251  addcos  12252  subcos  12253  cos2tsin  12257  ef01bndlem  12262  sin01bnd  12263  cos01bnd  12264  absef  12276  absefib  12277  efieq1re  12278  demoivre  12279  demoivreALT  12280  odd2np1lem  12378  odd2np1  12379  opoe  12401  omoe  12402  opeo  12403  omeo  12404  modgcd  12507  qredeq  12613  modprm0  12772  pythagtriplem1  12783  pythagtriplem12  12793  pythagtriplem14  12795  gzmulcl  12896  4sqlem11  12919  4sqlem17  12925  cncrng  14527  cnfldmulg  14534  mpomulcn  15234  mulc1cncf  15257  mulcncflem  15275  dvmulxxbr  15370  dvmulxx  15372  dvimulf  15374  plymullem1  15416  plymulcl  15423  plysubcl  15424  efper  15475  sinperlem  15476  sin2kpi  15479  cos2kpi  15480  efimpi  15487  sincosq1eq  15507  abssinper  15514  sinkpi  15515  coskpi  15516  binom4  15647  fsumdvdsmul  15659  lgsdilem2  15709  lgsne0  15711  lgsquadlem1  15750  2sqlem2  15788