ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  mulcl Structured version   GIF version

Theorem mulcl 6806
Description: Alias for ax-mulcl 6781, for naming consistency with mulcli 6830. (Contributed by NM, 10-Mar-2008.)
Assertion
Ref Expression
mulcl ((A B ℂ) → (A · B) ℂ)

Proof of Theorem mulcl
StepHypRef Expression
1 ax-mulcl 6781 1 ((A B ℂ) → (A · B) ℂ)
Colors of variables: wff set class
Syntax hints:  wi 4   wa 97   wcel 1390  (class class class)co 5455  cc 6709   · cmul 6716
This theorem was proved from axioms:  ax-mulcl 6781
This theorem is referenced by:  0cn  6817  mulid1  6822  mulcli  6830  mulcld  6845  mul31  6941  mul4  6942  cnegexlem2  6984  cnegex  6986  muladd  7177  subdi  7178  mul02  7180  submul2  7192  mulsub  7194  recextlem1  7414  recexap  7416  muleqadd  7431  divassap  7451  divmuldivap  7470  divmuleqap  7475  divadddivap  7485  conjmulap  7487  cju  7694  zneo  8115  expivallem  8910  expival  8911  exp1  8915  expp1  8916  expcl  8927  expclzaplem  8933  mulexp  8948  sqcl  8969  subsq  9011  subsq2  9012  binom2sub  9017  binom3  9019  zesq  9020  bernneq  9022  bernneq2  9023  reim  9080  imcl  9082  crre  9085  crim  9086  remim  9088  mulreap  9092  cjreb  9094  recj  9095  reneg  9096  readd  9097  remullem  9099  remul2  9101  imcj  9103  imneg  9104  imadd  9105  immul2  9108  cjadd  9112  ipcnval  9114  cjmulrcl  9115  cjneg  9118  imval2  9122  cjreim  9131  rennim  9211
  Copyright terms: Public domain W3C validator