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

Theorem mulcli 7883
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 7859 . 2 ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 · 𝐵) ∈ ℂ)
41, 2, 3mp2an 423 1 (𝐴 · 𝐵) ∈ ℂ
Colors of variables: wff set class
Syntax hints:  wcel 2128  (class class class)co 5824  cc 7730   · cmul 7737
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia3 107  ax-mulcl 7830
This theorem is referenced by:  ixi  8458  2mulicn  9055  numma  9338  nummac  9339  9t11e99  9424  decbin2  9435  irec  10518  binom2i  10527  3dec  10588  rei  10799  imi  10800  3dvdsdec  11756  3dvds2dec  11757  odd2np1  11764  3lcm2e6woprm  11963  6lcm4e12  11964  sinhalfpilem  13123  ef2pi  13137  ef2kpi  13138  efper  13139  sinperlem  13140  sin2kpi  13143  cos2kpi  13144  sin2pim  13145  cos2pim  13146  sincos4thpi  13172  sincos6thpi  13174  abssinper  13178  cosq34lt1  13182
  Copyright terms: Public domain W3C validator