Theorem mulcl 7771

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

Syntax hints:   -> wi 4   /\ wa 103   e. wcel 1481  (class class class)co 5782   CCcc 7642   x. cmul 7649

This theorem was proved from axioms:  ax-mulcl 7742

This theorem is referenced by:  0cn  7782  mulid1  7787  mulcli  7795  mulcld  7810  mul31  7917  mul4  7918  muladd11r  7942  cnegexlem2  7962  cnegex  7964  muladd  8170  subdi  8171  mul02  8173  submul2  8185  mulsub  8187  recextlem1  8436  recexap  8438  muleqadd  8453  divassap  8474  divmulassap  8479  divmuldivap  8496  divmuleqap  8501  divadddivap  8511  conjmulap  8513  cju  8743  zneo  9176  exp3vallem  10325  exp3val  10326  exp1  10330  expp1  10331  expcl  10342  expclzaplem  10348  mulexp  10363  sqcl  10385  subsq  10430  subsq2  10431  binom2sub  10436  mulbinom2  10439  binom3  10440  zesq  10441  bernneq  10443  bernneq2  10444  facnn  10505  fac0  10506  fac1  10507  facp1  10508  bcval5  10541  bcn2  10542  reim  10656  imcl  10658  crre  10661  crim  10662  remim  10664  mulreap  10668  cjreb  10670  recj  10671  reneg  10672  readd  10673  remullem  10675  remul2  10677  imcj  10679  imneg  10680  imadd  10681  immul2  10684  cjadd  10688  ipcnval  10690  cjmulrcl  10691  cjneg  10694  imval2  10698  cjreim  10707  rennim  10806  sqabsadd  10859  sqabssub  10860  absreimsq  10871  absreim  10872  absmul  10873  mul0inf  11044  mulcn2  11113  climmul  11128  isermulc2  11141  fsummulc2  11249  prodf  11339  clim2prod  11340  clim2divap  11341  prod3fmul  11342  prodf1  11343  prodfap0  11346  prodfrecap  11347  prodrbdclem  11372  fproddccvg  11373  prodmodclem3  11376  prodmodclem2a  11377  zproddc  11380  fprodseq  11384  efexp  11425  sinf  11447  cosf  11448  tanval2ap  11456  tanval3ap  11457  resinval  11458  recosval  11459  efi4p  11460  resin4p  11461  recos4p  11462  resincl  11463  recoscl  11464  sinneg  11469  cosneg  11470  efival  11475  efmival  11476  efeul  11477  sinadd  11479  cosadd  11480  sinsub  11483  cossub  11484  subsin  11486  sinmul  11487  cosmul  11488  addcos  11489  subcos  11490  cos2tsin  11494  ef01bndlem  11499  sin01bnd  11500  cos01bnd  11501  absef  11512  absefib  11513  efieq1re  11514  demoivre  11515  demoivreALT  11516  odd2np1lem  11605  odd2np1  11606  opoe  11628  omoe  11629  opeo  11630  omeo  11631  modgcd  11715  qredeq  11813  mulc1cncf  12784  mulcncflem  12798  dvmulxxbr  12874  dvmulxx  12876  dvimulf  12878  efper  12936  sinperlem  12937  sin2kpi  12940  cos2kpi  12941  efimpi  12948  sincosq1eq  12968  abssinper  12975  sinkpi  12976  coskpi  12977