Theorem mulcomli 11267

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

Syntax hints:   = wceq 1536   ∈ wcel 2105  (class class class)co 7430  ℂcc 11150   · cmul 11157

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-9 2115  ax-ext 2705  ax-mulcom 11216

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1776  df-cleq 2726

This theorem is referenced by:  divcan1i  12008  mvllmuli  12097  recgt0ii  12171  nummul2c  12780  halfthird  12873  5recm6rec  12874  sq4e2t8  14234  cos2bnd  16220  prmo3  17074  dec5nprm  17099  decexp2  17108  karatsuba  17117  2exp6  17120  2exp8  17122  2exp11  17123  2exp16  17124  7prm  17144  13prm  17149  17prm  17150  19prm  17151  23prm  17152  43prm  17155  83prm  17156  139prm  17157  163prm  17158  317prm  17159  631prm  17160  1259lem1  17164  1259lem2  17165  1259lem3  17166  1259lem4  17167  1259lem5  17168  1259prm  17169  2503lem1  17170  2503lem2  17171  2503lem3  17172  2503prm  17173  4001lem1  17174  4001lem2  17175  4001lem3  17176  4001lem4  17177  4001prm  17178  pcoass  25070  efif1olem2  26599  mcubic  26904  quart1lem  26912  quart1  26913  quartlem1  26914  tanatan  26976  log2ublem3  27005  log2ub  27006  cht3  27230  bclbnd  27338  bpos1lem  27340  bposlem4  27345  bposlem5  27346  bposlem8  27349  2lgslem3a  27454  2lgsoddprmlem3c  27470  2lgsoddprmlem3d  27471  ex-exp  30478  ex-fac  30479  ex-prmo  30487  ipasslem10  30867  siii  30881  normlem3  31140  bcsiALT  31207  dpmul1000  32865  hgt750lem2  34645  12lcm5e60  41989  60lcm7e420  41991  420lcm8e840  41992  3exp7  42034  3lexlogpow5ineq1  42035  3lexlogpow2ineq2  42040  3lexlogpow5ineq5  42041  aks4d1p1  42057  4t5e20  42304  235t711  42317  ex-decpmul  42318  0tie0  42328  3cubeslem3l  42673  3cubeslem3r  42674  sqrtcval2  43631  resqrtvalex  43634  inductionexd  44144  fouriersw  46186  1t10e1p1e11  47259  fmtno5lem1  47477  fmtno5lem2  47478  257prm  47485  fmtno4prmfac  47496  fmtno4nprmfac193  47498  fmtno5faclem2  47504  139prmALT  47520  127prm  47523  mod42tp1mod8  47526  3exp4mod41  47540  41prothprmlem2  47542  2exp340mod341  47657  8exp8mod9  47660  gpg5order  47948