Theorem mulcl 7532

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

Syntax hints:   -> wi 4   /\ wa 103   e. wcel 1439  (class class class)co 5668   CCcc 7411   x. cmul 7418

This theorem was proved from axioms:  ax-mulcl 7506

This theorem is referenced by:  0cn  7543  mulid1  7548  mulcli  7556  mulcld  7571  mul31  7676  mul4  7677  muladd11r  7701  cnegexlem2  7721  cnegex  7723  muladd  7925  subdi  7926  mul02  7928  submul2  7940  mulsub  7942  recextlem1  8183  recexap  8185  muleqadd  8200  divassap  8220  divmulassap  8225  divmuldivap  8242  divmuleqap  8247  divadddivap  8257  conjmulap  8259  cju  8484  zneo  8910  exp3vallem  10019  exp3val  10020  exp1  10024  expp1  10025  expcl  10036  expclzaplem  10042  mulexp  10057  sqcl  10079  subsq  10124  subsq2  10125  binom2sub  10130  mulbinom2  10133  binom3  10134  zesq  10135  bernneq  10137  bernneq2  10138  facnn  10198  fac0  10199  fac1  10200  facp1  10201  ibcval5  10234  bcn2  10235  reim  10349  imcl  10351  crre  10354  crim  10355  remim  10357  mulreap  10361  cjreb  10363  recj  10364  reneg  10365  readd  10366  remullem  10368  remul2  10370  imcj  10372  imneg  10373  imadd  10374  immul2  10377  cjadd  10381  ipcnval  10383  cjmulrcl  10384  cjneg  10387  imval2  10391  cjreim  10400  rennim  10498  sqabsadd  10551  sqabssub  10552  absreimsq  10563  absreim  10564  absmul  10565  mulcn2  10764  climmul  10778  iisermulc2  10791  fsummulc2  10905  efexp  11035  sinf  11058  cosf  11059  tanval2ap  11067  tanval3ap  11068  resinval  11069  recosval  11070  efi4p  11071  resin4p  11072  recos4p  11073  resincl  11074  recoscl  11075  sinneg  11080  cosneg  11081  efival  11086  efmival  11087  efeul  11088  sinadd  11090  cosadd  11091  sinsub  11094  cossub  11095  subsin  11097  sinmul  11098  cosmul  11099  addcos  11100  subcos  11101  cos2tsin  11105  ef01bndlem  11110  sin01bnd  11111  cos01bnd  11112  absef  11122  absefib  11123  efieq1re  11124  demoivre  11125  demoivreALT  11126  odd2np1lem  11213  odd2np1  11214  opoe  11236  omoe  11237  opeo  11238  omeo  11239  modgcd  11323  qredeq  11419  mulc1cncf  11949