Theorem mulcl 7913

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

Syntax hints:   -> wi 4   /\ wa 104   e. wcel 2146  (class class class)co 5865   CCcc 7784   x. cmul 7791

This theorem was proved from axioms:  ax-mulcl 7884

This theorem is referenced by:  0cn  7924  mulid1  7929  mulcli  7937  mulcld  7952  mul31  8062  mul4  8063  muladd11r  8087  cnegexlem2  8107  cnegex  8109  muladd  8315  subdi  8316  mul02  8318  submul2  8330  mulsub  8332  recextlem1  8581  recexap  8583  muleqadd  8598  divassap  8620  divmulassap  8625  divmuldivap  8642  divmuleqap  8647  divadddivap  8657  conjmulap  8659  cju  8891  zneo  9327  exp3vallem  10491  exp3val  10492  exp1  10496  expp1  10497  expcl  10508  expclzaplem  10514  mulexp  10529  sqcl  10551  subsq  10596  subsq2  10597  binom2sub  10603  mulbinom2  10606  binom3  10607  zesq  10608  bernneq  10610  bernneq2  10611  facnn  10675  fac0  10676  fac1  10677  facp1  10678  bcval5  10711  bcn2  10712  reim  10829  imcl  10831  crre  10834  crim  10835  remim  10837  mulreap  10841  cjreb  10843  recj  10844  reneg  10845  readd  10846  remullem  10848  remul2  10850  imcj  10852  imneg  10853  imadd  10854  immul2  10857  cjadd  10861  ipcnval  10863  cjmulrcl  10864  cjneg  10867  imval2  10871  cjreim  10880  rennim  10979  sqabsadd  11032  sqabssub  11033  absreimsq  11044  absreim  11045  absmul  11046  mul0inf  11217  mulcn2  11288  climmul  11303  isermulc2  11316  fsummulc2  11424  prodf  11514  clim2prod  11515  clim2divap  11516  prod3fmul  11517  prodf1  11518  prodfap0  11521  prodfrecap  11522  prodrbdclem  11547  fproddccvg  11548  prodmodclem3  11551  prodmodclem2a  11552  zproddc  11555  fprodseq  11559  fprodntrivap  11560  prodsnf  11568  fprodcl  11583  fprodclf  11611  efexp  11658  sinf  11680  cosf  11681  tanval2ap  11689  tanval3ap  11690  resinval  11691  recosval  11692  efi4p  11693  resin4p  11694  recos4p  11695  resincl  11696  recoscl  11697  sinneg  11702  cosneg  11703  efival  11708  efmival  11709  efeul  11710  sinadd  11712  cosadd  11713  sinsub  11716  cossub  11717  subsin  11719  sinmul  11720  cosmul  11721  addcos  11722  subcos  11723  cos2tsin  11727  ef01bndlem  11732  sin01bnd  11733  cos01bnd  11734  absef  11745  absefib  11746  efieq1re  11747  demoivre  11748  demoivreALT  11749  odd2np1lem  11844  odd2np1  11845  opoe  11867  omoe  11868  opeo  11869  omeo  11870  modgcd  11959  qredeq  12063  modprm0  12221  pythagtriplem1  12232  pythagtriplem12  12242  pythagtriplem14  12244  gzmulcl  12343  mulc1cncf  13647  mulcncflem  13661  dvmulxxbr  13737  dvmulxx  13739  dvimulf  13741  efper  13799  sinperlem  13800  sin2kpi  13803  cos2kpi  13804  efimpi  13811  sincosq1eq  13831  abssinper  13838  sinkpi  13839  coskpi  13840  binom4  13968  lgsdilem2  14008  lgsne0  14010  2sqlem2  14022