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

Theorem mulcomd 7488
Description: Commutative 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
mulcomd  |-  ( ph  ->  ( A  x.  B
)  =  ( B  x.  A ) )

Proof of Theorem mulcomd
StepHypRef Expression
1 addcld.1 . 2  |-  ( ph  ->  A  e.  CC )
2 addcld.2 . 2  |-  ( ph  ->  B  e.  CC )
3 mulcom 7450 . 2  |-  ( ( A  e.  CC  /\  B  e.  CC )  ->  ( A  x.  B
)  =  ( B  x.  A ) )
41, 2, 3syl2anc 403 1  |-  ( ph  ->  ( A  x.  B
)  =  ( B  x.  A ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1289    e. wcel 1438  (class class class)co 5634   CCcc 7327    x. cmul 7334
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia3 106  ax-mulcom 7425
This theorem is referenced by:  mul31  7592  remulext2  8053  mulreim  8057  mulext2  8066  mulcanapd  8104  mulcanap2d  8105  divcanap1  8122  divrecap2  8130  div23ap  8132  divdivdivap  8154  divmuleqap  8158  divadddivap  8168  divcanap5rd  8257  dmdcanap2d  8260  mvllmulapd  8276  prodgt0  8285  lt2mul2div  8312  mulle0r  8377  qapne  9093  modqvalr  9697  modqcyc  9731  mulp1mod1  9737  modqmul12d  9750  modqnegd  9751  modqmulmodr  9762  addmodlteq  9770  expaddzap  9964  binom2  10030  binom3  10036  bccmpl  10127  bcm1k  10133  bcn2  10137  bcpasc  10139  cvg1nlemcxze  10380  cvg1nlemcau  10382  resqrexlemcalc1  10412  resqrexlemcalc2  10413  resqrexlemnm  10416  recvalap  10495  isummulc1  10784  fsummulc1  10806  trireciplem  10855  geolim  10866  cvgratnnlemnexp  10879  cvgratnnlemmn  10880  cvgratnnlemfm  10884  cvgratz  10887  nndivides  10896  dvds2ln  10922  even2n  10967  oddm1even  10968  m1exp1  10994  divalgmod  11020  mulgcdr  11100  rplpwr  11109  lcmgcdlem  11152  divgcdcoprmex  11177  cncongr1  11178  oddpwdclemxy  11240  2sqpwodd  11247  evenennn  11299
  Copyright terms: Public domain W3C validator