Theorem mulcomd 8194

Description: Commutative law for multiplication. (Contributed by Mario Carneiro, 27-May-2016.)

Hypotheses

Ref	Expression
addcld.1	⊢ (𝜑 → 𝐴 ∈ ℂ)
addcld.2	⊢ (𝜑 → 𝐵 ∈ ℂ)

Assertion

Ref	Expression
mulcomd	⊢ (𝜑 → (𝐴 · 𝐵) = (𝐵 · 𝐴))

Proof of Theorem mulcomd

Step	Hyp	Ref	Expression
1		addcld.1	. 2 ⊢ (𝜑 → 𝐴 ∈ ℂ)
2		addcld.2	. 2 ⊢ (𝜑 → 𝐵 ∈ ℂ)
3		mulcom 8154	. 2 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 · 𝐵) = (𝐵 · 𝐴))
4	1, 2, 3	syl2anc 411	1 ⊢ (𝜑 → (𝐴 · 𝐵) = (𝐵 · 𝐴))

Syntax hints:   → wi 4   = wceq 1395   ∈ wcel 2200  (class class class)co 6013  ℂcc 8023   · cmul 8030

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

This theorem is referenced by:  mul31  8303  remulext2  8773  mulreim  8777  mulext2  8786  mulcanapd  8834  mulcanap2d  8835  divcanap1  8854  divrecap2  8862  div23ap  8864  divdivdivap  8886  divmuleqap  8890  divadddivap  8900  apmul2  8962  apdivmuld  8986  divcanap5rd  8991  dmdcanap2d  8994  mvllmulapd  9015  prodgt0  9025  lt2mul2div  9052  mulle0r  9117  subhalfhalf  9372  qapne  9866  irrmulap  9875  mul2lt0llt0  9989  mul2lt0lgt0  9990  mul2lt0pn  9992  modqvalr  10580  modqcyc  10614  mulp1mod1  10620  modqmul12d  10633  modqnegd  10634  modqmulmodr  10645  addmodlteq  10653  expaddzap  10838  binom2  10906  binom3  10912  bccmpl  11009  bcm1k  11015  bcn2  11019  bcpasc  11021  cvg1nlemcxze  11536  cvg1nlemcau  11538  resqrexlemcalc1  11568  resqrexlemcalc2  11569  resqrexlemnm  11572  recvalap  11651  bdtrilem  11793  reccn2ap  11867  isummulc1  11981  fsummulc1  12003  trireciplem  12054  geolim  12065  cvgratnnlemnexp  12078  cvgratnnlemmn  12079  cvgratnnlemfm  12083  cvgratz  12086  mertensabs  12091  eftlub  12244  sinadd  12290  cosadd  12291  sin2t  12303  nndivides  12351  dvds2ln  12378  even2n  12428  oddm1even  12429  m1exp1  12455  divalgmod  12481  bitsp1  12505  bitsinv1lem  12515  mulgcdr  12582  rplpwr  12591  lcmgcdlem  12642  divgcdcoprmex  12667  cncongr1  12668  oddpwdclemxy  12734  2sqpwodd  12741  eulerthlema  12795  eulerthlemth  12797  prmdiv  12800  prmdivdiv  12802  modprmn0modprm0  12822  coprimeprodsq  12823  pythagtriplem6  12836  pythagtriplem7  12837  pceulem  12860  pcadd  12906  prmpwdvds  12921  mul4sqlem  12959  4sqlem17  12973  evenennn  13007  mulgassr  13740  znunit  14666  dvmulxxbr  15419  dvmptcmulcn  15438  dvply1  15482  tangtx  15555  cxpmul  15629  abscxp  15632  binom4  15696  wilthlem1  15697  mpodvdsmulf1o  15707  sgmppw  15709  perfect1  15715  lgsdirprm  15756  lgsdi  15759  lgsdirnn0  15769  lgsdinn0  15770  gausslemma2dlem1a  15780  gausslemma2dlem6  15789  lgsquadlem1  15799  lgsquadlem2  15800  lgsquadlem3  15801  lgsquad2  15805  2lgslem3a1  15819  2lgslem3b1  15820  2lgslem3c1  15821  2lgslem3d1  15822  2lgsoddprmlem2  15828  2sqlem3  15839  2sqlem4  15840