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

Theorem mulcli 7493
Description: Closure law for multiplication. (Contributed by NM, 23-Nov-1994.)
Hypotheses
Ref Expression
axi.1 𝐴 ∈ ℂ
axi.2 𝐵 ∈ ℂ
Assertion
Ref Expression
mulcli (𝐴 · 𝐵) ∈ ℂ

Proof of Theorem mulcli
StepHypRef Expression
1 axi.1 . 2 𝐴 ∈ ℂ
2 axi.2 . 2 𝐵 ∈ ℂ
3 mulcl 7469 . 2 ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 · 𝐵) ∈ ℂ)
41, 2, 3mp2an 417 1 (𝐴 · 𝐵) ∈ ℂ
Colors of variables: wff set class
Syntax hints:  wcel 1438  (class class class)co 5652  cc 7348   · cmul 7355
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia3 106  ax-mulcl 7443
This theorem is referenced by:  ixi  8060  2mulicn  8638  numma  8920  nummac  8921  9t11e99  9006  decbin2  9017  irec  10054  binom2i  10063  3dec  10123  rei  10333  imi  10334  3dvdsdec  11143  3dvds2dec  11144  odd2np1  11151  3lcm2e6woprm  11346  6lcm4e12  11347
  Copyright terms: Public domain W3C validator