Theorem mulcomli 11152

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

Syntax hints:   = wceq 1547   ∈ wcel 2119  (class class class)co 7363  ℂcc 11034   · cmul 11041

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-9 2129  ax-ext 2712  ax-mulcom 11100

This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1787  df-cleq 2732

This theorem is referenced by:  divcan1i  11897  mvllmuli  11986  recgt0ii  12060  halfthird  12396  nummul2c  12692  5recm6rec  12785  sq4e2t8  14159  cos2bnd  16153  prmo3  17010  dec5nprm  17035  karatsuba  17052  2exp6  17055  2exp8  17057  2exp11  17058  2exp16  17059  7prm  17079  13prm  17084  17prm  17085  19prm  17086  23prm  17087  43prm  17090  83prm  17091  139prm  17092  163prm  17093  317prm  17094  631prm  17095  1259lem1  17099  1259lem2  17100  1259lem3  17101  1259lem4  17102  1259lem5  17103  1259prm  17104  2503lem1  17105  2503lem2  17106  2503lem3  17107  2503prm  17108  4001lem1  17109  4001lem2  17110  4001lem3  17111  4001lem4  17112  4001prm  17113  pcoass  25016  efif1olem2  26532  mcubic  26836  quart1lem  26844  quart1  26845  quartlem1  26846  tanatan  26908  log2ublem3  26937  log2ub  26938  cht3  27161  bclbnd  27268  bpos1lem  27270  bposlem4  27275  bposlem5  27276  bposlem8  27279  2lgslem3a  27384  2lgsoddprmlem3c  27400  2lgsoddprmlem3d  27401  ex-exp  30545  ex-fac  30546  ex-prmo  30554  ipasslem10  30935  siii  30949  normlem3  31208  bcsiALT  31275  dpmul1000  32984  hgt750lem2  34843  12lcm5e60  42500  60lcm7e420  42502  420lcm8e840  42503  3exp7  42545  3lexlogpow5ineq1  42546  3lexlogpow2ineq2  42551  3lexlogpow5ineq5  42552  aks4d1p1  42568  4t5e20  42775  235t711  42789  ex-decpmul  42790  0tie0  42799  3cubeslem3l  43142  3cubeslem3r  43143  sqrtcval2  44093  resqrtvalex  44096  inductionexd  44606  fouriersw  46681  goldrasin  47352  1t10e1p1e11  47780  fmtno5lem1  48038  fmtno5lem2  48039  257prm  48046  fmtno4prmfac  48057  fmtno4nprmfac193  48059  fmtno5faclem2  48065  139prmALT  48081  127prm  48084  mod42tp1mod8  48087  3exp4mod41  48101  41prothprmlem2  48103  2exp340mod341  48231  8exp8mod9  48234  gpg5order  48558