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

Theorem mulcld 6845
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 6806 . 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 6709   · cmul 6716
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia3 101  ax-mulcl 6781
This theorem is referenced by:  kcnktkm1cn  7176  rereim  7370  cru  7386  apreim  7387  mulreim  7388  apadd1  7392  apneg  7395  mulext1  7396  mulext  7398  mulap0  7417  receuap  7432  divrecap  7449  divcanap3  7457  divdivdivap  7471  divsubdivap  7486  apmul1  7546  qapne  8350  cnref1o  8357  lincmb01cmp  8641  iccf1o  8642  mulexpzap  8949  expmulzap  8955  binom2  9015  binom3  9019  bernneq  9022  remullem  9099  cjreim2  9132  cnrecnv  9138  absval  9210
  Copyright terms: Public domain W3C validator