Theorem mulcomli 11188

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

Syntax hints:   = wceq 1559   ∈ wcel 2141  (class class class)co 7392  ℂcc 11068   · cmul 11075

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-9 2151  ax-ext 2733  ax-mulcom 11134

This theorem depends on definitions:  df-bi 209  df-an 400  df-ex 1799  df-cleq 2753

This theorem is referenced by:  divcan1i  11932  mvllmuli  12021  recgt0ii  12095  2t3e6  12381  2t4e8  12384  halfthird  12439  nummul2c  12740  5recm6rec  12835  sq4e2t8  14209  cos2bnd  16203  prmo3  17060  dec5nprm  17085  karatsuba  17102  2exp6  17105  2exp8  17107  2exp11  17108  2exp16  17109  7prm  17129  13prm  17135  17prm  17136  19prm  17137  23prm  17138  43prm  17141  83prm  17142  139prm  17143  163prm  17144  317prm  17145  631prm  17146  1259lem1  17150  1259lem2  17151  1259lem3  17152  1259lem4  17153  1259lem5  17154  1259prm  17155  2503lem1  17156  2503lem2  17157  2503lem3  17158  2503prm  17159  4001lem1  17160  4001lem2  17161  4001lem3  17162  4001lem4  17163  4001prm  17164  pcoass  25066  efif1olem2  26585  mcubic  26889  quart1lem  26897  quart1  26898  quartlem1  26899  tanatan  26961  log2ublem3  26990  log2ub  26991  bclbnd  27321  bpos1lem  27323  bposlem4  27328  bposlem5  27329  bposlem8  27332  2lgslem3a  27437  2lgsoddprmlem3c  27453  2lgsoddprmlem3d  27454  ex-exp  30598  ex-fac  30599  ex-prmo  30607  ipasslem10  30988  siii  31002  normlem3  31261  bcsiALT  31328  dpmul1000  33037  hgt750lem2  34910  12lcm5e60  42589  60lcm7e420  42591  420lcm8e840  42592  3exp7  42634  3lexlogpow5ineq1  42635  3lexlogpow2ineq2  42640  3lexlogpow5ineq5  42641  aks4d1p1  42657  4t5e20  42864  235t711  42878  ex-decpmul  42879  0tie0  42888  3cubeslem3l  43231  3cubeslem3r  43232  sqrtcval2  44182  resqrtvalex  44185  inductionexd  44695  fouriersw  46769  goldrasin  47440  1t10e1p1e11  47868  fmtno5lem1  48126  fmtno5lem2  48127  257prm  48134  fmtno4prmfac  48145  fmtno4nprmfac193  48147  fmtno5faclem2  48153  139prmALT  48169  127prm  48172  3exp4mod41  48189  41prothprmlem2  48191  2exp340mod341  48319  8exp8mod9  48322  gpg5order  48646