Theorem mulcomd 8347

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 8308	. 2 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 · 𝐵) = (𝐵 · 𝐴))
4	1, 2, 3	syl2anc 415	1 ⊢ (𝜑 → (𝐴 · 𝐵) = (𝐵 · 𝐴))

This proof depends on syntax axioms:   → wi 4   = wceq 1402   ∈ wcel 2209  (class class class)co 6085  ℂcc 8177   · cmul 8184

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia3 108  ax-mulcom 8280

This theorem is used by:  mul31  8458  remulext2  8930  mulreim  8934  mulext2  8943  mulcanapd  8991  mulcanap2d  8992  divcanap1  9013  divrecap2  9021  div23ap  9023  divdivdivap  9045  divmuleqap  9049  divadddivap  9059  apmul2  9121  apdivmuld  9145  divcanap5rd  9150  dmdcanap2d  9153  mvllmulapd  9174  prodgt0  9184  lt2mul2div  9211  mulle0r  9276  subhalfhalf  9544  qapne  10048  irrmulap  10058  mul2lt0llt0  10172  mul2lt0lgt0  10173  mul2lt0pn  10175  modqvalr  10775  modqcyc  10809  mulp1mod1  10815  modqmul12d  10828  modqnegd  10829  modqmulmodr  10840  addmodlteq  10848  expaddzap  11033  binom2  11101  binom3  11107  bccmpl  11206  bcm1k  11212  bcn2  11216  bcpasc  11218  cvg1nlemcxze  11762  cvg1nlemcau  11764  resqrexlemcalc1  11794  resqrexlemcalc2  11795  resqrexlemnm  11798  recvalap  11878  bdtrilem  12021  reccn2ap  12095  isummulc1  12210  fsummulc1  12232  trireciplem  12283  geolim  12294  cvgratnnlemnexp  12307  cvgratnnlemmn  12308  cvgratnnlemfm  12312  cvgratz  12315  mertensabs  12320  eftlub  12473  sinadd  12519  cosadd  12520  sin2t  12532  nndivides  12580  dvds2ln  12607  even2n  12657  oddm1even  12658  m1exp1  12684  divalgmod  12710  bitsp1  12734  bitsinv1lem  12744  mulgcdr  12811  rplpwr  12820  lcmgcdlem  12871  divgcdcoprmex  12896  cncongr1  12897  nnmaxpwlemxy  12964  2sqpwodd  12972  eulerthlema  13028  eulerthlemth  13030  prmdiv  13033  prmdivdiv  13035  modprmn0modprm0  13055  coprimeprodsq  13056  pythagtriplem6  13069  pythagtriplem7  13070  pceulem  13093  pcadd  13139  prmpwdvds  13154  mul4sqlem  13192  4sqlem17  13206  evenennn  13333  mulgassr  14012  znunit  15043  dvmulxxbr  15852  dvmptcmulcn  15871  dvply1  15915  tangtx  15989  logdivlt  16046  cxpmul  16067  abscxp  16070  binom4  16138  pellexlem2  16149  wilthlem1  16151  mpodvdsmulf1o  16203  sgmppw  16205  perfect1  16217  lgsdirprm  16272  lgsdi  16275  lgsdirnn0  16285  lgsdinn0  16286  gausslemma2dlem1a  16296  gausslemma2dlem6  16305  lgsquadlem1  16315  lgsquadlem2  16316  lgsquadlem3  16317  lgsquad2  16321  2lgslem3a1  16335  2lgslem3b1  16336  2lgslem3c1  16337  2lgslem3d1  16338  2lgsoddprmlem2  16344  2sqlem3  16355  2sqlem4  16356  dichmul0orlem3  16874