Theorem mulcl 8051

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

Syntax hints:   -> wi 4   /\ wa 104   e. wcel 2175  (class class class)co 5943   CCcc 7922   x. cmul 7929

This theorem was proved from axioms:  ax-mulcl 8022

This theorem is referenced by:  mpomulf  8061  0cn  8063  mulrid  8068  mulcli  8076  mulcld  8092  mul31  8202  mul4  8203  muladd11r  8227  cnegexlem2  8247  cnegex  8249  muladd  8455  subdi  8456  mul02  8458  submul2  8470  mulsub  8472  recextlem1  8723  recexap  8725  muleqadd  8740  divassap  8762  divmulassap  8767  divmuldivap  8784  divmuleqap  8789  divadddivap  8799  conjmulap  8801  cju  9033  ofnegsub  9034  zneo  9473  exp3vallem  10683  exp3val  10684  exp1  10688  expp1  10689  expcl  10700  expclzaplem  10706  mulexp  10721  sqcl  10743  subsq  10789  subsq2  10790  binom2sub  10796  mulbinom2  10799  binom3  10800  zesq  10801  bernneq  10803  bernneq2  10804  mulsubdivbinom2ap  10854  facnn  10870  fac0  10871  fac1  10872  facp1  10873  bcval5  10906  bcn2  10907  reim  11134  imcl  11136  crre  11139  crim  11140  remim  11142  mulreap  11146  cjreb  11148  recj  11149  reneg  11150  readd  11151  remullem  11153  remul2  11155  imcj  11157  imneg  11158  imadd  11159  immul2  11162  cjadd  11166  ipcnval  11168  cjmulrcl  11169  cjneg  11172  imval2  11176  cjreim  11185  rennim  11284  sqabsadd  11337  sqabssub  11338  absreimsq  11349  absreim  11350  absmul  11351  mul0inf  11523  mulcn2  11594  climmul  11609  isermulc2  11622  fsummulc2  11730  prodf  11820  clim2prod  11821  clim2divap  11822  prod3fmul  11823  prodf1  11824  prodfap0  11827  prodfrecap  11828  prodrbdclem  11853  fproddccvg  11854  prodmodclem3  11857  prodmodclem2a  11858  zproddc  11861  fprodseq  11865  fprodntrivap  11866  prodsnf  11874  fprodcl  11889  fprodclf  11917  efexp  11964  sinf  11986  cosf  11987  tanval2ap  11995  tanval3ap  11996  resinval  11997  recosval  11998  efi4p  11999  resin4p  12000  recos4p  12001  resincl  12002  recoscl  12003  sinneg  12008  cosneg  12009  efival  12014  efmival  12015  efeul  12016  sinadd  12018  cosadd  12019  sinsub  12022  cossub  12023  subsin  12025  sinmul  12026  cosmul  12027  addcos  12028  subcos  12029  cos2tsin  12033  ef01bndlem  12038  sin01bnd  12039  cos01bnd  12040  absef  12052  absefib  12053  efieq1re  12054  demoivre  12055  demoivreALT  12056  odd2np1lem  12154  odd2np1  12155  opoe  12177  omoe  12178  opeo  12179  omeo  12180  modgcd  12283  qredeq  12389  modprm0  12548  pythagtriplem1  12559  pythagtriplem12  12569  pythagtriplem14  12571  gzmulcl  12672  4sqlem11  12695  4sqlem17  12701  cncrng  14302  cnfldmulg  14309  mpomulcn  15009  mulc1cncf  15032  mulcncflem  15050  dvmulxxbr  15145  dvmulxx  15147  dvimulf  15149  plymullem1  15191  plymulcl  15198  plysubcl  15199  efper  15250  sinperlem  15251  sin2kpi  15254  cos2kpi  15255  efimpi  15262  sincosq1eq  15282  abssinper  15289  sinkpi  15290  coskpi  15291  binom4  15422  fsumdvdsmul  15434  lgsdilem2  15484  lgsne0  15486  lgsquadlem1  15525  2sqlem2  15563