Theorem mulcl 7969

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

Syntax hints:   -> wi 4   /\ wa 104   e. wcel 2160  (class class class)co 5897   CCcc 7840   x. cmul 7847

This theorem was proved from axioms:  ax-mulcl 7940

This theorem is referenced by:  0cn  7980  mulrid  7985  mulcli  7993  mulcld  8009  mul31  8119  mul4  8120  muladd11r  8144  cnegexlem2  8164  cnegex  8166  muladd  8372  subdi  8373  mul02  8375  submul2  8387  mulsub  8389  recextlem1  8639  recexap  8641  muleqadd  8656  divassap  8678  divmulassap  8683  divmuldivap  8700  divmuleqap  8705  divadddivap  8715  conjmulap  8717  cju  8949  zneo  9385  exp3vallem  10555  exp3val  10556  exp1  10560  expp1  10561  expcl  10572  expclzaplem  10578  mulexp  10593  sqcl  10615  subsq  10661  subsq2  10662  binom2sub  10668  mulbinom2  10671  binom3  10672  zesq  10673  bernneq  10675  bernneq2  10676  mulsubdivbinom2ap  10726  facnn  10742  fac0  10743  fac1  10744  facp1  10745  bcval5  10778  bcn2  10779  reim  10896  imcl  10898  crre  10901  crim  10902  remim  10904  mulreap  10908  cjreb  10910  recj  10911  reneg  10912  readd  10913  remullem  10915  remul2  10917  imcj  10919  imneg  10920  imadd  10921  immul2  10924  cjadd  10928  ipcnval  10930  cjmulrcl  10931  cjneg  10934  imval2  10938  cjreim  10947  rennim  11046  sqabsadd  11099  sqabssub  11100  absreimsq  11111  absreim  11112  absmul  11113  mul0inf  11284  mulcn2  11355  climmul  11370  isermulc2  11383  fsummulc2  11491  prodf  11581  clim2prod  11582  clim2divap  11583  prod3fmul  11584  prodf1  11585  prodfap0  11588  prodfrecap  11589  prodrbdclem  11614  fproddccvg  11615  prodmodclem3  11618  prodmodclem2a  11619  zproddc  11622  fprodseq  11626  fprodntrivap  11627  prodsnf  11635  fprodcl  11650  fprodclf  11678  efexp  11725  sinf  11747  cosf  11748  tanval2ap  11756  tanval3ap  11757  resinval  11758  recosval  11759  efi4p  11760  resin4p  11761  recos4p  11762  resincl  11763  recoscl  11764  sinneg  11769  cosneg  11770  efival  11775  efmival  11776  efeul  11777  sinadd  11779  cosadd  11780  sinsub  11783  cossub  11784  subsin  11786  sinmul  11787  cosmul  11788  addcos  11789  subcos  11790  cos2tsin  11794  ef01bndlem  11799  sin01bnd  11800  cos01bnd  11801  absef  11812  absefib  11813  efieq1re  11814  demoivre  11815  demoivreALT  11816  odd2np1lem  11912  odd2np1  11913  opoe  11935  omoe  11936  opeo  11937  omeo  11938  modgcd  12027  qredeq  12131  modprm0  12289  pythagtriplem1  12300  pythagtriplem12  12310  pythagtriplem14  12312  gzmulcl  12413  4sqlem11  12436  4sqlem17  12442  cncrng  13889  cnfldmulg  13896  mulc1cncf  14553  mulcncflem  14567  dvmulxxbr  14643  dvmulxx  14645  dvimulf  14647  efper  14705  sinperlem  14706  sin2kpi  14709  cos2kpi  14710  efimpi  14717  sincosq1eq  14737  abssinper  14744  sinkpi  14745  coskpi  14746  binom4  14874  lgsdilem2  14915  lgsne0  14917  2sqlem2  14940