Theorem mulcomi 11344

Description: Commutative law for multiplication. (Contributed by NM, 23-Nov-1994.)

Hypotheses

Ref	Expression
axi.1	⊢ 𝐴 ∈ ℂ
axi.2	⊢ 𝐵 ∈ ℂ

Assertion

Ref	Expression
mulcomi	⊢ (𝐴 · 𝐵) = (𝐵 · 𝐴)

Proof of Theorem mulcomi

Step	Hyp	Ref	Expression
1		axi.1	. 2 ⊢ 𝐴 ∈ ℂ
2		axi.2	. 2 ⊢ 𝐵 ∈ ℂ
3		mulcom 11313	. 2 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 · 𝐵) = (𝐵 · 𝐴))
4	1, 2, 3	mp2an 705	1 ⊢ (𝐴 · 𝐵) = (𝐵 · 𝐴)

This proof depends on syntax axioms:   = wceq 1570   ∈ wcel 2147  (class class class)co 7443  ℂcc 11225   · cmul 11232

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-mulcom 11291

This proof depends on definitions:  df-bi 210  df-an 402

This theorem is used by:  mulcomli  11345  divmul13i  12105  8th4div3  12593  numma2c  12892  nummul2c  12896  9t11e99OLD  12977  binom2i  14383  tanval2  16330  pockthi  17114  mod2xnegi  17278  decsplit1  17288  decsplit  17289  83prm  17330  dvsincos  26331  sincosq4sgn  26860  2logb9irrALT  27156  ang180lem3  27169  mcubic  27205  cubic2  27206  log2ublem2  27305  log2ublem3  27306  log2ub  27307  chtub  27569  bposlem8  27648  2lgsoddprmlem2  27766  2lgsoddprmlem3d  27770  ax5seglem7  29543  ex-ind-dvds  31092  ipdirilem  31461  siilem1  31483  bcseqi  31752  h1de2i  32185  dpmul10  33531  dpmul4  33550  signswch  35260  hgt750lem  35350  hgt750lem2  35351  problem4  36600  problem5  36601  quad3  36602  mulcomnni  43229  lcmineqlem23  43293  3lexlogpow5ineq1  43296  arearect  44409  areaquad  44410  wallispilem4  47283  dirkercncflem1  47318  fourierswlem  47445  goldpolyfactor  48132  goldratmolem2  48138  257prm  48851  fmtno4prmfac  48862  5tcu2e40  48905  41prothprm  48909  tgoldbachlt  49119  zlmodzxzequap  49816