Theorem mulcomd 7911

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

Syntax hints:   → wi 4   = wceq 1342   ∈ wcel 2135  (class class class)co 5836  ℂcc 7742   · cmul 7749

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

This theorem is referenced by:  mul31  8020  remulext2  8489  mulreim  8493  mulext2  8502  mulcanapd  8549  mulcanap2d  8550  divcanap1  8568  divrecap2  8576  div23ap  8578  divdivdivap  8600  divmuleqap  8604  divadddivap  8614  apmul2  8676  apdivmuld  8700  divcanap5rd  8705  dmdcanap2d  8708  mvllmulapd  8729  prodgt0  8738  lt2mul2div  8765  mulle0r  8830  qapne  9568  mul2lt0llt0  9688  mul2lt0lgt0  9689  mul2lt0pn  9691  modqvalr  10250  modqcyc  10284  mulp1mod1  10290  modqmul12d  10303  modqnegd  10304  modqmulmodr  10315  addmodlteq  10323  expaddzap  10489  binom2  10555  binom3  10561  bccmpl  10656  bcm1k  10662  bcn2  10666  bcpasc  10668  cvg1nlemcxze  10910  cvg1nlemcau  10912  resqrexlemcalc1  10942  resqrexlemcalc2  10943  resqrexlemnm  10946  recvalap  11025  bdtrilem  11166  reccn2ap  11240  isummulc1  11354  fsummulc1  11376  trireciplem  11427  geolim  11438  cvgratnnlemnexp  11451  cvgratnnlemmn  11452  cvgratnnlemfm  11456  cvgratz  11459  mertensabs  11464  eftlub  11617  sinadd  11663  cosadd  11664  sin2t  11676  nndivides  11723  dvds2ln  11750  even2n  11796  oddm1even  11797  m1exp1  11823  divalgmod  11849  mulgcdr  11936  rplpwr  11945  lcmgcdlem  11988  divgcdcoprmex  12013  cncongr1  12014  oddpwdclemxy  12078  2sqpwodd  12085  eulerthlema  12139  eulerthlemth  12141  prmdiv  12144  prmdivdiv  12146  modprmn0modprm0  12165  coprimeprodsq  12166  pythagtriplem6  12179  pythagtriplem7  12180  pceulem  12203  pcadd  12248  evenennn  12263  dvmulxxbr  13207  dvmptcmulcn  13224  tangtx  13300  cxpmul  13374  abscxp  13376  binom4  13438