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

Theorem mulcli 7735
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 7711 . 2 ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 · 𝐵) ∈ ℂ)
41, 2, 3mp2an 420 1 (𝐴 · 𝐵) ∈ ℂ
Colors of variables: wff set class
Syntax hints:  wcel 1463  (class class class)co 5740  cc 7582   · cmul 7589
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia3 107  ax-mulcl 7682
This theorem is referenced by:  ixi  8308  2mulicn  8896  numma  9179  nummac  9180  9t11e99  9265  decbin2  9276  irec  10343  binom2i  10352  3dec  10412  rei  10622  imi  10623  3dvdsdec  11469  3dvds2dec  11470  odd2np1  11477  3lcm2e6woprm  11674  6lcm4e12  11675
  Copyright terms: Public domain W3C validator