Theorem mulcomi 11252

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 11224	. 2 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 · 𝐵) = (𝐵 · 𝐴))
4	1, 2, 3	mp2an 691	1 ⊢ (𝐴 · 𝐵) = (𝐵 · 𝐴)

Syntax hints:   = wceq 1534   ∈ wcel 2099  (class class class)co 7420  ℂcc 11136   · cmul 11143

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-mulcom 11202

This theorem depends on definitions:  df-bi 206  df-an 396

This theorem is referenced by:  mulcomli  11253  divmul13i  12005  8th4div3  12462  numma2c  12753  nummul2c  12757  9t11e99  12837  binom2i  14207  fac3  14271  tanval2  16109  pockthi  16875  mod2xnegi  17039  decexp2  17043  decsplit1  17050  decsplit  17051  83prm  17091  dvsincos  25912  sincosq4sgn  26435  2logb9irrALT  26729  ang180lem3  26742  mcubic  26778  cubic2  26779  log2ublem2  26878  log2ublem3  26879  log2ub  26880  basellem8  27019  ppiub  27136  chtub  27144  bposlem8  27223  2lgsoddprmlem2  27341  2lgsoddprmlem3d  27345  ax5seglem7  28745  ex-ind-dvds  30270  ipdirilem  30638  siilem1  30660  bcseqi  30929  h1de2i  31362  dpmul10  32618  dpmul4  32637  signswch  34193  hgt750lem  34283  hgt750lem2  34284  problem4  35272  problem5  35273  quad3  35274  mulcomnni  41458  lcmineqlem23  41522  3lexlogpow5ineq1  41525  arearect  42643  areaquad  42644  wallispilem4  45456  dirkercncflem1  45491  fourierswlem  45618  257prm  46901  fmtno4prmfac  46912  5tcu2e40  46955  41prothprm  46959  tgoldbachlt  47156  zlmodzxzequap  47567

Otomatik - 173.255.232.114 CloudFlare DNS Türk Telekom DNS Google DNS Open DNS

OSZAR »