Theorem mulcl 7940

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

Syntax hints:   -> wi 4   /\ wa 104   e. wcel 2148  (class class class)co 5877   CCcc 7811   x. cmul 7818

This theorem was proved from axioms:  ax-mulcl 7911

This theorem is referenced by:  0cn  7951  mulrid  7956  mulcli  7964  mulcld  7980  mul31  8090  mul4  8091  muladd11r  8115  cnegexlem2  8135  cnegex  8137  muladd  8343  subdi  8344  mul02  8346  submul2  8358  mulsub  8360  recextlem1  8610  recexap  8612  muleqadd  8627  divassap  8649  divmulassap  8654  divmuldivap  8671  divmuleqap  8676  divadddivap  8686  conjmulap  8688  cju  8920  zneo  9356  exp3vallem  10523  exp3val  10524  exp1  10528  expp1  10529  expcl  10540  expclzaplem  10546  mulexp  10561  sqcl  10583  subsq  10629  subsq2  10630  binom2sub  10636  mulbinom2  10639  binom3  10640  zesq  10641  bernneq  10643  bernneq2  10644  mulsubdivbinom2ap  10693  facnn  10709  fac0  10710  fac1  10711  facp1  10712  bcval5  10745  bcn2  10746  reim  10863  imcl  10865  crre  10868  crim  10869  remim  10871  mulreap  10875  cjreb  10877  recj  10878  reneg  10879  readd  10880  remullem  10882  remul2  10884  imcj  10886  imneg  10887  imadd  10888  immul2  10891  cjadd  10895  ipcnval  10897  cjmulrcl  10898  cjneg  10901  imval2  10905  cjreim  10914  rennim  11013  sqabsadd  11066  sqabssub  11067  absreimsq  11078  absreim  11079  absmul  11080  mul0inf  11251  mulcn2  11322  climmul  11337  isermulc2  11350  fsummulc2  11458  prodf  11548  clim2prod  11549  clim2divap  11550  prod3fmul  11551  prodf1  11552  prodfap0  11555  prodfrecap  11556  prodrbdclem  11581  fproddccvg  11582  prodmodclem3  11585  prodmodclem2a  11586  zproddc  11589  fprodseq  11593  fprodntrivap  11594  prodsnf  11602  fprodcl  11617  fprodclf  11645  efexp  11692  sinf  11714  cosf  11715  tanval2ap  11723  tanval3ap  11724  resinval  11725  recosval  11726  efi4p  11727  resin4p  11728  recos4p  11729  resincl  11730  recoscl  11731  sinneg  11736  cosneg  11737  efival  11742  efmival  11743  efeul  11744  sinadd  11746  cosadd  11747  sinsub  11750  cossub  11751  subsin  11753  sinmul  11754  cosmul  11755  addcos  11756  subcos  11757  cos2tsin  11761  ef01bndlem  11766  sin01bnd  11767  cos01bnd  11768  absef  11779  absefib  11780  efieq1re  11781  demoivre  11782  demoivreALT  11783  odd2np1lem  11879  odd2np1  11880  opoe  11902  omoe  11903  opeo  11904  omeo  11905  modgcd  11994  qredeq  12098  modprm0  12256  pythagtriplem1  12267  pythagtriplem12  12277  pythagtriplem14  12279  gzmulcl  12378  cncrng  13548  cnfldmulg  13555  mulc1cncf  14161  mulcncflem  14175  dvmulxxbr  14251  dvmulxx  14253  dvimulf  14255  efper  14313  sinperlem  14314  sin2kpi  14317  cos2kpi  14318  efimpi  14325  sincosq1eq  14345  abssinper  14352  sinkpi  14353  coskpi  14354  binom4  14482  lgsdilem2  14522  lgsne0  14524  2sqlem2  14547