Theorem mulcomli 11228

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

Hypotheses

Ref	Expression
axi.1	⊢ 𝐴 ∈ ℂ
axi.2	⊢ 𝐵 ∈ ℂ
mulcomli.3	⊢ (𝐴 · 𝐵) = 𝐶

Assertion

Ref	Expression
mulcomli	⊢ (𝐵 · 𝐴) = 𝐶

Proof of Theorem mulcomli

Step	Hyp	Ref	Expression
1		axi.2	. . 3 ⊢ 𝐵 ∈ ℂ
2		axi.1	. . 3 ⊢ 𝐴 ∈ ℂ
3	1, 2	mulcomi 11227	. 2 ⊢ (𝐵 · 𝐴) = (𝐴 · 𝐵)
4		mulcomli.3	. 2 ⊢ (𝐴 · 𝐵) = 𝐶
5	3, 4	eqtri 2759	1 ⊢ (𝐵 · 𝐴) = 𝐶

Syntax hints:   = wceq 1540   ∈ wcel 2105  (class class class)co 7412  ℂcc 11111   · cmul 11118

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1912  ax-6 1970  ax-7 2010  ax-9 2115  ax-ext 2702  ax-mulcom 11177

This theorem depends on definitions:  df-bi 206  df-an 396  df-ex 1781  df-cleq 2723

This theorem is referenced by:  divcan1i  11963  mvllmuli  12052  recgt0ii  12125  nummul2c  12732  halfthird  12825  5recm6rec  12826  sq4e2t8  14168  cos2bnd  16136  prmo3  16979  dec5nprm  17004  decexp2  17013  karatsuba  17022  2exp6  17025  2exp8  17027  2exp11  17028  2exp16  17029  7prm  17049  13prm  17054  17prm  17055  19prm  17056  23prm  17057  43prm  17060  83prm  17061  139prm  17062  163prm  17063  317prm  17064  631prm  17065  1259lem1  17069  1259lem2  17070  1259lem3  17071  1259lem4  17072  1259lem5  17073  1259prm  17074  2503lem1  17075  2503lem2  17076  2503lem3  17077  2503prm  17078  4001lem1  17079  4001lem2  17080  4001lem3  17081  4001lem4  17082  4001prm  17083  pcoass  24772  efif1olem2  26289  mcubic  26589  quart1lem  26597  quart1  26598  quartlem1  26599  tanatan  26661  log2ublem3  26690  log2ub  26691  cht3  26914  bclbnd  27020  bpos1lem  27022  bposlem4  27027  bposlem5  27028  bposlem8  27031  2lgslem3a  27136  2lgsoddprmlem3c  27152  2lgsoddprmlem3d  27153  ex-exp  29971  ex-fac  29972  ex-prmo  29980  ipasslem10  30360  siii  30374  normlem3  30633  bcsiALT  30700  dpmul1000  32333  hgt750lem2  33963  12lcm5e60  41180  60lcm7e420  41182  420lcm8e840  41183  3exp7  41225  3lexlogpow5ineq1  41226  3lexlogpow2ineq2  41231  3lexlogpow5ineq5  41232  aks4d1p1  41248  4t5e20  41506  235t711  41508  ex-decpmul  41509  3cubeslem3l  41727  3cubeslem3r  41728  sqrtcval2  42696  resqrtvalex  42699  inductionexd  43209  fouriersw  45246  1t10e1p1e11  46317  fmtno5lem1  46520  fmtno5lem2  46521  257prm  46528  fmtno4prmfac  46539  fmtno4nprmfac193  46541  fmtno5faclem2  46547  139prmALT  46563  127prm  46566  mod42tp1mod8  46569  3exp4mod41  46583  41prothprmlem2  46585  2exp340mod341  46700  8exp8mod9  46703