Theorem mulcomd 7140

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 7102	. 2 |- ( ( A e. CC /\ B e. CC ) -> ( A x. B ) = ( B x. A ) )
4	1, 2, 3	syl2anc 403	1 |- ( ph -> ( A x. B ) = ( B x. A ) )

Syntax hints:   -> wi 4   = wceq 1284   e. wcel 1433  (class class class)co 5532   CCcc 6979   x. cmul 6986

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

This theorem is referenced by:  mul31  7239  remulext2  7700  mulreim  7704  mulext2  7713  mulcanapd  7751  mulcanap2d  7752  divcanap1  7769  divrecap2  7777  div23ap  7779  divdivdivap  7801  divmuleqap  7805  divadddivap  7815  divcanap5rd  7904  dmdcanap2d  7907  mvllmulapd  7921  prodgt0  7930  lt2mul2div  7957  mulle0r  8022  qapne  8724  modqvalr  9327  modqcyc  9361  mulp1mod1  9367  modqmul12d  9380  modqnegd  9381  modqmulmodr  9392  addmodlteq  9400  expaddzap  9520  binom2  9585  binom3  9590  bccmpl  9681  bcm1k  9687  bcn2  9691  bcpasc  9693  cvg1nlemcxze  9868  cvg1nlemcau  9870  resqrexlemcalc1  9900  resqrexlemcalc2  9901  resqrexlemnm  9904  recvalap  9983  nndivides  10202  dvds2ln  10228  even2n  10273  oddm1even  10274  m1exp1  10301  divalgmod  10327  mulgcdr  10407  rplpwr  10416  lcmgcdlem  10459  divgcdcoprmex  10484  cncongr1  10485  oddpwdclemxy  10547  2sqpwodd  10554