Theorem mulcomd 7979

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

Syntax hints:   → wi 4   = wceq 1353   ∈ wcel 2148  (class class class)co 5875  ℂcc 7809   · cmul 7816

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

This theorem is referenced by:  mul31  8088  remulext2  8557  mulreim  8561  mulext2  8570  mulcanapd  8618  mulcanap2d  8619  divcanap1  8638  divrecap2  8646  div23ap  8648  divdivdivap  8670  divmuleqap  8674  divadddivap  8684  apmul2  8746  apdivmuld  8770  divcanap5rd  8775  dmdcanap2d  8778  mvllmulapd  8799  prodgt0  8809  lt2mul2div  8836  mulle0r  8901  qapne  9639  mul2lt0llt0  9761  mul2lt0lgt0  9762  mul2lt0pn  9764  modqvalr  10325  modqcyc  10359  mulp1mod1  10365  modqmul12d  10378  modqnegd  10379  modqmulmodr  10390  addmodlteq  10398  expaddzap  10564  binom2  10632  binom3  10638  bccmpl  10734  bcm1k  10740  bcn2  10744  bcpasc  10746  cvg1nlemcxze  10991  cvg1nlemcau  10993  resqrexlemcalc1  11023  resqrexlemcalc2  11024  resqrexlemnm  11027  recvalap  11106  bdtrilem  11247  reccn2ap  11321  isummulc1  11435  fsummulc1  11457  trireciplem  11508  geolim  11519  cvgratnnlemnexp  11532  cvgratnnlemmn  11533  cvgratnnlemfm  11537  cvgratz  11540  mertensabs  11545  eftlub  11698  sinadd  11744  cosadd  11745  sin2t  11757  nndivides  11804  dvds2ln  11831  even2n  11879  oddm1even  11880  m1exp1  11906  divalgmod  11932  mulgcdr  12019  rplpwr  12028  lcmgcdlem  12077  divgcdcoprmex  12102  cncongr1  12103  oddpwdclemxy  12169  2sqpwodd  12176  eulerthlema  12230  eulerthlemth  12232  prmdiv  12235  prmdivdiv  12237  modprmn0modprm0  12256  coprimeprodsq  12257  pythagtriplem6  12270  pythagtriplem7  12271  pceulem  12294  pcadd  12339  prmpwdvds  12353  mul4sqlem  12391  evenennn  12394  mulgassr  13021  dvmulxxbr  14169  dvmptcmulcn  14186  tangtx  14262  cxpmul  14336  abscxp  14338  binom4  14400  lgsdirprm  14438  lgsdi  14441  lgsdirnn0  14451  lgsdinn0  14452  2lgsoddprmlem2  14457  2sqlem3  14467  2sqlem4  14468