Theorem mulcl 7100

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

Syntax hints:   -> wi 4   /\ wa 102   e. wcel 1433  (class class class)co 5532   CCcc 6979   x. cmul 6986

This theorem was proved from axioms:  ax-mulcl 7074

This theorem is referenced by:  0cn  7111  mulid1  7116  mulcli  7124  mulcld  7139  mul31  7239  mul4  7240  muladd11r  7264  cnegexlem2  7284  cnegex  7286  muladd  7488  subdi  7489  mul02  7491  submul2  7503  mulsub  7505  recextlem1  7741  recexap  7743  muleqadd  7758  divassap  7778  divmulassap  7783  divmuldivap  7800  divmuleqap  7805  divadddivap  7815  conjmulap  7817  cju  8038  zneo  8448  expivallem  9477  expival  9478  exp1  9482  expp1  9483  expcl  9494  expclzaplem  9500  mulexp  9515  sqcl  9537  subsq  9581  subsq2  9582  binom2sub  9587  mulbinom2  9589  binom3  9590  zesq  9591  bernneq  9593  bernneq2  9594  facnn  9654  fac0  9655  fac1  9656  facp1  9657  ibcval5  9690  bcn2  9691  reim  9739  imcl  9741  crre  9744  crim  9745  remim  9747  mulreap  9751  cjreb  9753  recj  9754  reneg  9755  readd  9756  remullem  9758  remul2  9760  imcj  9762  imneg  9763  imadd  9764  immul2  9767  cjadd  9771  ipcnval  9773  cjmulrcl  9774  cjneg  9777  imval2  9781  cjreim  9790  rennim  9888  sqabsadd  9941  sqabssub  9942  absreimsq  9953  absreim  9954  absmul  9955  mulcn2  10151  climmul  10165  iisermulc2  10178  odd2np1lem  10271  odd2np1  10272  opoe  10295  omoe  10296  opeo  10297  omeo  10298  modgcd  10382  qredeq  10478