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

Theorem mulcli 7925
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 7901 . 2 ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 · 𝐵) ∈ ℂ)
41, 2, 3mp2an 424 1 (𝐴 · 𝐵) ∈ ℂ
Colors of variables: wff set class
Syntax hints:  wcel 2141  (class class class)co 5853  cc 7772   · cmul 7779
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia3 107  ax-mulcl 7872
This theorem is referenced by:  ixi  8502  2mulicn  9100  numma  9386  nummac  9387  9t11e99  9472  decbin2  9483  irec  10575  binom2i  10584  3dec  10648  rei  10863  imi  10864  3dvdsdec  11824  3dvds2dec  11825  odd2np1  11832  3lcm2e6woprm  12040  6lcm4e12  12041  sinhalfpilem  13506  ef2pi  13520  ef2kpi  13521  efper  13522  sinperlem  13523  sin2kpi  13526  cos2kpi  13527  sin2pim  13528  cos2pim  13529  sincos4thpi  13555  sincos6thpi  13557  abssinper  13561  cosq34lt1  13565  lgsdir2lem5  13727
  Copyright terms: Public domain W3C validator