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

Theorem mulcld 6805
Description: Closure law for multiplication. (Contributed by Mario Carneiro, 27-May-2016.)
Hypotheses
Ref Expression
addcld.1 (φA ℂ)
addcld.2 (φB ℂ)
Assertion
Ref Expression
mulcld (φ → (A · B) ℂ)

Proof of Theorem mulcld
StepHypRef Expression
1 addcld.1 . 2 (φA ℂ)
2 addcld.2 . 2 (φB ℂ)
3 mulcl 6766 . 2 ((A B ℂ) → (A · B) ℂ)
41, 2, 3syl2anc 391 1 (φ → (A · B) ℂ)
Colors of variables: wff set class
Syntax hints:  wi 4   wcel 1390  (class class class)co 5455  cc 6669   · cmul 6676
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia3 101  ax-mulcl 6741
This theorem is referenced by:  kcnktkm1cn  7136  rereim  7330  cru  7346  apreim  7347  mulreim  7348  apadd1  7352  apneg  7355  mulext1  7356  mulext  7358  mulap0  7377  receuap  7392  divrecap  7409  divcanap3  7417  divdivdivap  7431  divsubdivap  7446  apmul1  7506  qapne  8310  cnref1o  8317  lincmb01cmp  8601  iccf1o  8602  mulexpzap  8909  expmulzap  8915  binom2  8975  binom3  8979  bernneq  8982  remullem  9059  cjreim2  9092  cnrecnv  9098
  Copyright terms: Public domain W3C validator