Theorem mulcomli 11154

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

Syntax hints:   = wceq 1542   ∈ wcel 2114  (class class class)co 7367  ℂ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 2708  ax-mulcom 11102

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

This theorem is referenced by:  divcan1i  11899  mvllmuli  11988  recgt0ii  12062  halfthird  12398  nummul2c  12694  5recm6rec  12787  sq4e2t8  14161  cos2bnd  16155  prmo3  17012  dec5nprm  17037  karatsuba  17054  2exp6  17057  2exp8  17059  2exp11  17060  2exp16  17061  7prm  17081  13prm  17086  17prm  17087  19prm  17088  23prm  17089  43prm  17092  83prm  17093  139prm  17094  163prm  17095  317prm  17096  631prm  17097  1259lem1  17101  1259lem2  17102  1259lem3  17103  1259lem4  17104  1259lem5  17105  1259prm  17106  2503lem1  17107  2503lem2  17108  2503lem3  17109  2503prm  17110  4001lem1  17111  4001lem2  17112  4001lem3  17113  4001lem4  17114  4001prm  17115  pcoass  24991  efif1olem2  26507  mcubic  26811  quart1lem  26819  quart1  26820  quartlem1  26821  tanatan  26883  log2ublem3  26912  log2ub  26913  cht3  27136  bclbnd  27243  bpos1lem  27245  bposlem4  27250  bposlem5  27251  bposlem8  27254  2lgslem3a  27359  2lgsoddprmlem3c  27375  2lgsoddprmlem3d  27376  ex-exp  30520  ex-fac  30521  ex-prmo  30529  ipasslem10  30910  siii  30924  normlem3  31183  bcsiALT  31250  dpmul1000  32958  hgt750lem2  34796  12lcm5e60  42447  60lcm7e420  42449  420lcm8e840  42450  3exp7  42492  3lexlogpow5ineq1  42493  3lexlogpow2ineq2  42498  3lexlogpow5ineq5  42499  aks4d1p1  42515  4t5e20  42723  235t711  42737  ex-decpmul  42738  0tie0  42747  3cubeslem3l  43118  3cubeslem3r  43119  sqrtcval2  44069  resqrtvalex  44072  inductionexd  44582  fouriersw  46659  goldrasin  47330  1t10e1p1e11  47758  fmtno5lem1  48016  fmtno5lem2  48017  257prm  48024  fmtno4prmfac  48035  fmtno4nprmfac193  48037  fmtno5faclem2  48043  139prmALT  48059  127prm  48062  mod42tp1mod8  48065  3exp4mod41  48079  41prothprmlem2  48081  2exp340mod341  48209  8exp8mod9  48212  gpg5order  48536