Theorem mulcl 7876

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

Syntax hints:   -> wi 4   /\ wa 103   e. wcel 2136  (class class class)co 5841   CCcc 7747   x. cmul 7754

This theorem was proved from axioms:  ax-mulcl 7847

This theorem is referenced by:  0cn  7887  mulid1  7892  mulcli  7900  mulcld  7915  mul31  8025  mul4  8026  muladd11r  8050  cnegexlem2  8070  cnegex  8072  muladd  8278  subdi  8279  mul02  8281  submul2  8293  mulsub  8295  recextlem1  8544  recexap  8546  muleqadd  8561  divassap  8582  divmulassap  8587  divmuldivap  8604  divmuleqap  8609  divadddivap  8619  conjmulap  8621  cju  8852  zneo  9288  exp3vallem  10452  exp3val  10453  exp1  10457  expp1  10458  expcl  10469  expclzaplem  10475  mulexp  10490  sqcl  10512  subsq  10557  subsq2  10558  binom2sub  10564  mulbinom2  10567  binom3  10568  zesq  10569  bernneq  10571  bernneq2  10572  facnn  10636  fac0  10637  fac1  10638  facp1  10639  bcval5  10672  bcn2  10673  reim  10790  imcl  10792  crre  10795  crim  10796  remim  10798  mulreap  10802  cjreb  10804  recj  10805  reneg  10806  readd  10807  remullem  10809  remul2  10811  imcj  10813  imneg  10814  imadd  10815  immul2  10818  cjadd  10822  ipcnval  10824  cjmulrcl  10825  cjneg  10828  imval2  10832  cjreim  10841  rennim  10940  sqabsadd  10993  sqabssub  10994  absreimsq  11005  absreim  11006  absmul  11007  mul0inf  11178  mulcn2  11249  climmul  11264  isermulc2  11277  fsummulc2  11385  prodf  11475  clim2prod  11476  clim2divap  11477  prod3fmul  11478  prodf1  11479  prodfap0  11482  prodfrecap  11483  prodrbdclem  11508  fproddccvg  11509  prodmodclem3  11512  prodmodclem2a  11513  zproddc  11516  fprodseq  11520  fprodntrivap  11521  prodsnf  11529  fprodcl  11544  fprodclf  11572  efexp  11619  sinf  11641  cosf  11642  tanval2ap  11650  tanval3ap  11651  resinval  11652  recosval  11653  efi4p  11654  resin4p  11655  recos4p  11656  resincl  11657  recoscl  11658  sinneg  11663  cosneg  11664  efival  11669  efmival  11670  efeul  11671  sinadd  11673  cosadd  11674  sinsub  11677  cossub  11678  subsin  11680  sinmul  11681  cosmul  11682  addcos  11683  subcos  11684  cos2tsin  11688  ef01bndlem  11693  sin01bnd  11694  cos01bnd  11695  absef  11706  absefib  11707  efieq1re  11708  demoivre  11709  demoivreALT  11710  odd2np1lem  11805  odd2np1  11806  opoe  11828  omoe  11829  opeo  11830  omeo  11831  modgcd  11920  qredeq  12024  modprm0  12182  pythagtriplem1  12193  pythagtriplem12  12203  pythagtriplem14  12205  gzmulcl  12304  mulc1cncf  13176  mulcncflem  13190  dvmulxxbr  13266  dvmulxx  13268  dvimulf  13270  efper  13328  sinperlem  13329  sin2kpi  13332  cos2kpi  13333  efimpi  13340  sincosq1eq  13360  abssinper  13367  sinkpi  13368  coskpi  13369  binom4  13497  lgsdilem2  13537  lgsne0  13539  2sqlem2  13551