Theorem mulcomd 7705

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

Step	Hyp	Ref	Expression
1		addcld.1	. 2 |- ( ph -> A e. CC )
2		addcld.2	. 2 |- ( ph -> B e. CC )
3		mulcom 7667	. 2 |- ( ( A e. CC /\ B e. CC ) -> ( A x. B ) = ( B x. A ) )
4	1, 2, 3	syl2anc 406	1 |- ( ph -> ( A x. B ) = ( B x. A ) )

Syntax hints:   -> wi 4   = wceq 1312   e. wcel 1461  (class class class)co 5726   CCcc 7539   x. cmul 7546

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia3 107  ax-mulcom 7640

This theorem is referenced by:  mul31  7810  remulext2  8274  mulreim  8278  mulext2  8287  mulcanapd  8329  mulcanap2d  8330  divcanap1  8348  divrecap2  8356  div23ap  8358  divdivdivap  8380  divmuleqap  8384  divadddivap  8394  apmul2  8456  apdivmuld  8480  divcanap5rd  8485  dmdcanap2d  8488  mvllmulapd  8505  prodgt0  8514  lt2mul2div  8541  mulle0r  8606  qapne  9327  modqvalr  9985  modqcyc  10019  mulp1mod1  10025  modqmul12d  10038  modqnegd  10039  modqmulmodr  10050  addmodlteq  10058  expaddzap  10224  binom2  10290  binom3  10296  bccmpl  10387  bcm1k  10393  bcn2  10397  bcpasc  10399  cvg1nlemcxze  10640  cvg1nlemcau  10642  resqrexlemcalc1  10672  resqrexlemcalc2  10673  resqrexlemnm  10676  recvalap  10755  bdtrilem  10896  reccn2ap  10968  isummulc1  11082  fsummulc1  11104  trireciplem  11155  geolim  11166  cvgratnnlemnexp  11179  cvgratnnlemmn  11180  cvgratnnlemfm  11184  cvgratz  11187  mertensabs  11192  eftlub  11241  sinadd  11288  cosadd  11289  sin2t  11301  nndivides  11342  dvds2ln  11368  even2n  11413  oddm1even  11414  m1exp1  11440  divalgmod  11466  mulgcdr  11546  rplpwr  11555  lcmgcdlem  11598  divgcdcoprmex  11623  cncongr1  11624  oddpwdclemxy  11686  2sqpwodd  11693  evenennn  11745