Theorem mulcomli 11153

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 11152	. 2 ⊢ (𝐵 · 𝐴) = (𝐴 · 𝐵)
4		mulcomli.3	. 2 ⊢ (𝐴 · 𝐵) = 𝐶
5	3, 4	eqtri 2760	1 ⊢ (𝐵 · 𝐴) = 𝐶

Syntax hints:   = wceq 1542   ∈ wcel 2114  (class class class)co 7368  ℂcc 11036   · cmul 11043

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-9 2124  ax-ext 2709  ax-mulcom 11102

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-cleq 2729

This theorem is referenced by:  divcan1i  11897  mvllmuli  11986  recgt0ii  12060  halfthird  12374  nummul2c  12669  5recm6rec  12762  sq4e2t8  14134  cos2bnd  16125  prmo3  16981  dec5nprm  17006  karatsuba  17023  2exp6  17026  2exp8  17028  2exp11  17029  2exp16  17030  7prm  17050  13prm  17055  17prm  17056  19prm  17057  23prm  17058  43prm  17061  83prm  17062  139prm  17063  163prm  17064  317prm  17065  631prm  17066  1259lem1  17070  1259lem2  17071  1259lem3  17072  1259lem4  17073  1259lem5  17074  1259prm  17075  2503lem1  17076  2503lem2  17077  2503lem3  17078  2503prm  17079  4001lem1  17080  4001lem2  17081  4001lem3  17082  4001lem4  17083  4001prm  17084  pcoass  24992  efif1olem2  26520  mcubic  26825  quart1lem  26833  quart1  26834  quartlem1  26835  tanatan  26897  log2ublem3  26926  log2ub  26927  cht3  27151  bclbnd  27259  bpos1lem  27261  bposlem4  27266  bposlem5  27267  bposlem8  27270  2lgslem3a  27375  2lgsoddprmlem3c  27391  2lgsoddprmlem3d  27392  ex-exp  30537  ex-fac  30538  ex-prmo  30546  ipasslem10  30926  siii  30940  normlem3  31199  bcsiALT  31266  dpmul1000  32990  hgt750lem2  34829  12lcm5e60  42372  60lcm7e420  42374  420lcm8e840  42375  3exp7  42417  3lexlogpow5ineq1  42418  3lexlogpow2ineq2  42423  3lexlogpow5ineq5  42424  aks4d1p1  42440  4t5e20  42655  235t711  42669  ex-decpmul  42670  0tie0  42679  3cubeslem3l  43037  3cubeslem3r  43038  sqrtcval2  43992  resqrtvalex  43995  inductionexd  44505  fouriersw  46583  1t10e1p1e11  47664  fmtno5lem1  47907  fmtno5lem2  47908  257prm  47915  fmtno4prmfac  47926  fmtno4nprmfac193  47928  fmtno5faclem2  47934  139prmALT  47950  127prm  47953  mod42tp1mod8  47956  3exp4mod41  47970  41prothprmlem2  47972  2exp340mod341  48087  8exp8mod9  48090  gpg5order  48414