Theorem mulcl 8052

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

Syntax hints:   -> wi 4   /\ wa 104   e. wcel 2176  (class class class)co 5944   CCcc 7923   x. cmul 7930

This theorem was proved from axioms:  ax-mulcl 8023

This theorem is referenced by:  mpomulf  8062  0cn  8064  mulrid  8069  mulcli  8077  mulcld  8093  mul31  8203  mul4  8204  muladd11r  8228  cnegexlem2  8248  cnegex  8250  muladd  8456  subdi  8457  mul02  8459  submul2  8471  mulsub  8473  recextlem1  8724  recexap  8726  muleqadd  8741  divassap  8763  divmulassap  8768  divmuldivap  8785  divmuleqap  8790  divadddivap  8800  conjmulap  8802  cju  9034  ofnegsub  9035  zneo  9474  exp3vallem  10685  exp3val  10686  exp1  10690  expp1  10691  expcl  10702  expclzaplem  10708  mulexp  10723  sqcl  10745  subsq  10791  subsq2  10792  binom2sub  10798  mulbinom2  10801  binom3  10802  zesq  10803  bernneq  10805  bernneq2  10806  mulsubdivbinom2ap  10856  facnn  10872  fac0  10873  fac1  10874  facp1  10875  bcval5  10908  bcn2  10909  reim  11163  imcl  11165  crre  11168  crim  11169  remim  11171  mulreap  11175  cjreb  11177  recj  11178  reneg  11179  readd  11180  remullem  11182  remul2  11184  imcj  11186  imneg  11187  imadd  11188  immul2  11191  cjadd  11195  ipcnval  11197  cjmulrcl  11198  cjneg  11201  imval2  11205  cjreim  11214  rennim  11313  sqabsadd  11366  sqabssub  11367  absreimsq  11378  absreim  11379  absmul  11380  mul0inf  11552  mulcn2  11623  climmul  11638  isermulc2  11651  fsummulc2  11759  prodf  11849  clim2prod  11850  clim2divap  11851  prod3fmul  11852  prodf1  11853  prodfap0  11856  prodfrecap  11857  prodrbdclem  11882  fproddccvg  11883  prodmodclem3  11886  prodmodclem2a  11887  zproddc  11890  fprodseq  11894  fprodntrivap  11895  prodsnf  11903  fprodcl  11918  fprodclf  11946  efexp  11993  sinf  12015  cosf  12016  tanval2ap  12024  tanval3ap  12025  resinval  12026  recosval  12027  efi4p  12028  resin4p  12029  recos4p  12030  resincl  12031  recoscl  12032  sinneg  12037  cosneg  12038  efival  12043  efmival  12044  efeul  12045  sinadd  12047  cosadd  12048  sinsub  12051  cossub  12052  subsin  12054  sinmul  12055  cosmul  12056  addcos  12057  subcos  12058  cos2tsin  12062  ef01bndlem  12067  sin01bnd  12068  cos01bnd  12069  absef  12081  absefib  12082  efieq1re  12083  demoivre  12084  demoivreALT  12085  odd2np1lem  12183  odd2np1  12184  opoe  12206  omoe  12207  opeo  12208  omeo  12209  modgcd  12312  qredeq  12418  modprm0  12577  pythagtriplem1  12588  pythagtriplem12  12598  pythagtriplem14  12600  gzmulcl  12701  4sqlem11  12724  4sqlem17  12730  cncrng  14331  cnfldmulg  14338  mpomulcn  15038  mulc1cncf  15061  mulcncflem  15079  dvmulxxbr  15174  dvmulxx  15176  dvimulf  15178  plymullem1  15220  plymulcl  15227  plysubcl  15228  efper  15279  sinperlem  15280  sin2kpi  15283  cos2kpi  15284  efimpi  15291  sincosq1eq  15311  abssinper  15318  sinkpi  15319  coskpi  15320  binom4  15451  fsumdvdsmul  15463  lgsdilem2  15513  lgsne0  15515  lgsquadlem1  15554  2sqlem2  15592