Theorem mulcomd 7711

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

Syntax hints:   → wi 4   = wceq 1314   ∈ wcel 1463  (class class class)co 5728  ℂcc 7545   · cmul 7552

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

This theorem is referenced by:  mul31  7816  remulext2  8280  mulreim  8284  mulext2  8293  mulcanapd  8335  mulcanap2d  8336  divcanap1  8354  divrecap2  8362  div23ap  8364  divdivdivap  8386  divmuleqap  8390  divadddivap  8400  apmul2  8462  apdivmuld  8486  divcanap5rd  8491  dmdcanap2d  8494  mvllmulapd  8511  prodgt0  8520  lt2mul2div  8547  mulle0r  8612  qapne  9333  modqvalr  9991  modqcyc  10025  mulp1mod1  10031  modqmul12d  10044  modqnegd  10045  modqmulmodr  10056  addmodlteq  10064  expaddzap  10230  binom2  10296  binom3  10302  bccmpl  10393  bcm1k  10399  bcn2  10403  bcpasc  10405  cvg1nlemcxze  10646  cvg1nlemcau  10648  resqrexlemcalc1  10678  resqrexlemcalc2  10679  resqrexlemnm  10682  recvalap  10761  bdtrilem  10902  reccn2ap  10974  isummulc1  11088  fsummulc1  11110  trireciplem  11161  geolim  11172  cvgratnnlemnexp  11185  cvgratnnlemmn  11186  cvgratnnlemfm  11190  cvgratz  11193  mertensabs  11198  eftlub  11247  sinadd  11294  cosadd  11295  sin2t  11307  nndivides  11348  dvds2ln  11374  even2n  11419  oddm1even  11420  m1exp1  11446  divalgmod  11472  mulgcdr  11552  rplpwr  11561  lcmgcdlem  11604  divgcdcoprmex  11629  cncongr1  11630  oddpwdclemxy  11692  2sqpwodd  11699  evenennn  11751  dvmulxxbr  12621