Theorem mulcl 7747

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

Syntax hints:   -> wi 4   /\ wa 103   e. wcel 1480  (class class class)co 5774   CCcc 7618   x. cmul 7625

This theorem was proved from axioms:  ax-mulcl 7718

This theorem is referenced by:  0cn  7758  mulid1  7763  mulcli  7771  mulcld  7786  mul31  7893  mul4  7894  muladd11r  7918  cnegexlem2  7938  cnegex  7940  muladd  8146  subdi  8147  mul02  8149  submul2  8161  mulsub  8163  recextlem1  8412  recexap  8414  muleqadd  8429  divassap  8450  divmulassap  8455  divmuldivap  8472  divmuleqap  8477  divadddivap  8487  conjmulap  8489  cju  8719  zneo  9152  exp3vallem  10294  exp3val  10295  exp1  10299  expp1  10300  expcl  10311  expclzaplem  10317  mulexp  10332  sqcl  10354  subsq  10399  subsq2  10400  binom2sub  10405  mulbinom2  10408  binom3  10409  zesq  10410  bernneq  10412  bernneq2  10413  facnn  10473  fac0  10474  fac1  10475  facp1  10476  bcval5  10509  bcn2  10510  reim  10624  imcl  10626  crre  10629  crim  10630  remim  10632  mulreap  10636  cjreb  10638  recj  10639  reneg  10640  readd  10641  remullem  10643  remul2  10645  imcj  10647  imneg  10648  imadd  10649  immul2  10652  cjadd  10656  ipcnval  10658  cjmulrcl  10659  cjneg  10662  imval2  10666  cjreim  10675  rennim  10774  sqabsadd  10827  sqabssub  10828  absreimsq  10839  absreim  10840  absmul  10841  mul0inf  11012  mulcn2  11081  climmul  11096  isermulc2  11109  fsummulc2  11217  prodf  11307  clim2prod  11308  clim2divap  11309  prod3fmul  11310  prodf1  11311  prodfap0  11314  prodfrecap  11315  prodrbdclem  11340  fproddccvg  11341  prodmodclem3  11344  prodmodclem2a  11345  efexp  11388  sinf  11411  cosf  11412  tanval2ap  11420  tanval3ap  11421  resinval  11422  recosval  11423  efi4p  11424  resin4p  11425  recos4p  11426  resincl  11427  recoscl  11428  sinneg  11433  cosneg  11434  efival  11439  efmival  11440  efeul  11441  sinadd  11443  cosadd  11444  sinsub  11447  cossub  11448  subsin  11450  sinmul  11451  cosmul  11452  addcos  11453  subcos  11454  cos2tsin  11458  ef01bndlem  11463  sin01bnd  11464  cos01bnd  11465  absef  11476  absefib  11477  efieq1re  11478  demoivre  11479  demoivreALT  11480  odd2np1lem  11569  odd2np1  11570  opoe  11592  omoe  11593  opeo  11594  omeo  11595  modgcd  11679  qredeq  11777  mulc1cncf  12745  mulcncflem  12759  dvmulxxbr  12835  dvmulxx  12837  dvimulf  12839  efper  12888  sinperlem  12889  sin2kpi  12892  cos2kpi  12893  efimpi  12900  sincosq1eq  12920  abssinper  12927  sinkpi  12928  coskpi  12929