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

Theorem mulcld 7045
Description: Closure law for multiplication. (Contributed by Mario Carneiro, 27-May-2016.)
Hypotheses
Ref Expression
addcld.1  |-  ( ph  ->  A  e.  CC )
addcld.2  |-  ( ph  ->  B  e.  CC )
Assertion
Ref Expression
mulcld  |-  ( ph  ->  ( A  x.  B
)  e.  CC )

Proof of Theorem mulcld
StepHypRef Expression
1 addcld.1 . 2  |-  ( ph  ->  A  e.  CC )
2 addcld.2 . 2  |-  ( ph  ->  B  e.  CC )
3 mulcl 7006 . 2  |-  ( ( A  e.  CC  /\  B  e.  CC )  ->  ( A  x.  B
)  e.  CC )
41, 2, 3syl2anc 391 1  |-  ( ph  ->  ( A  x.  B
)  e.  CC )
Colors of variables: wff set class
Syntax hints:    -> wi 4    e. wcel 1393  (class class class)co 5512   CCcc 6885    x. cmul 6892
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia3 101  ax-mulcl 6980
This theorem is referenced by:  kcnktkm1cn  7378  rereim  7575  cru  7591  apreim  7592  mulreim  7593  apadd1  7597  apneg  7600  mulext1  7601  mulext  7603  mulap0  7633  receuap  7648  divrecap  7665  divcanap3  7673  divdivdivap  7687  divsubdivap  7702  apmul1  7762  qapne  8572  cnref1o  8580  lincmb01cmp  8869  iccf1o  8870  qbtwnrelemcalc  9108  mulexpzap  9269  expmulzap  9275  binom2  9336  binom3  9340  bernneq  9343  remullem  9445  cjreim2  9478  cnrecnv  9484  absval  9573  resqrexlemover  9582  resqrexlemcalc1  9586  resqrexlemnm  9590  absimle  9654  abstri  9674  mulcn2  9806  iisermulc2  9833  climcvg1nlem  9841
  Copyright terms: Public domain W3C validator