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

Theorem mulcli 7965
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 7941 . 2 ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 · 𝐵) ∈ ℂ)
41, 2, 3mp2an 426 1 (𝐴 · 𝐵) ∈ ℂ
Colors of variables: wff set class
Syntax hints:  wcel 2148  (class class class)co 5878  cc 7812   · cmul 7819
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia3 108  ax-mulcl 7912
This theorem is referenced by:  ixi  8543  2mulicn  9144  numma  9430  nummac  9431  9t11e99  9516  decbin2  9527  irec  10623  binom2i  10632  3dec  10697  rei  10911  imi  10912  3dvdsdec  11873  3dvds2dec  11874  odd2np1  11881  3lcm2e6woprm  12089  6lcm4e12  12090  sinhalfpilem  14373  ef2pi  14387  ef2kpi  14388  efper  14389  sinperlem  14390  sin2kpi  14393  cos2kpi  14394  sin2pim  14395  cos2pim  14396  sincos4thpi  14422  sincos6thpi  14424  abssinper  14428  cosq34lt1  14432  lgsdir2lem5  14594  2lgsoddprmlem3c  14618  2lgsoddprmlem3d  14619
  Copyright terms: Public domain W3C validator