Theorem mulcomli 11128

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

Syntax hints:   = wceq 1541   ∈ wcel 2113  (class class class)co 7352  ℂcc 11011   · cmul 11018

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-9 2123  ax-ext 2705  ax-mulcom 11077

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-cleq 2725

This theorem is referenced by:  divcan1i  11872  mvllmuli  11961  recgt0ii  12035  halfthird  12349  nummul2c  12644  5recm6rec  12737  sq4e2t8  14108  cos2bnd  16099  prmo3  16955  dec5nprm  16980  karatsuba  16997  2exp6  17000  2exp8  17002  2exp11  17003  2exp16  17004  7prm  17024  13prm  17029  17prm  17030  19prm  17031  23prm  17032  43prm  17035  83prm  17036  139prm  17037  163prm  17038  317prm  17039  631prm  17040  1259lem1  17044  1259lem2  17045  1259lem3  17046  1259lem4  17047  1259lem5  17048  1259prm  17049  2503lem1  17050  2503lem2  17051  2503lem3  17052  2503prm  17053  4001lem1  17054  4001lem2  17055  4001lem3  17056  4001lem4  17057  4001prm  17058  pcoass  24952  efif1olem2  26480  mcubic  26785  quart1lem  26793  quart1  26794  quartlem1  26795  tanatan  26857  log2ublem3  26886  log2ub  26887  cht3  27111  bclbnd  27219  bpos1lem  27221  bposlem4  27226  bposlem5  27227  bposlem8  27230  2lgslem3a  27335  2lgsoddprmlem3c  27351  2lgsoddprmlem3d  27352  ex-exp  30432  ex-fac  30433  ex-prmo  30441  ipasslem10  30821  siii  30835  normlem3  31094  bcsiALT  31161  dpmul1000  32886  hgt750lem2  34686  12lcm5e60  42121  60lcm7e420  42123  420lcm8e840  42124  3exp7  42166  3lexlogpow5ineq1  42167  3lexlogpow2ineq2  42172  3lexlogpow5ineq5  42173  aks4d1p1  42189  4t5e20  42409  235t711  42423  ex-decpmul  42424  0tie0  42433  3cubeslem3l  42803  3cubeslem3r  42804  sqrtcval2  43759  resqrtvalex  43762  inductionexd  44272  fouriersw  46353  1t10e1p1e11  47434  fmtno5lem1  47677  fmtno5lem2  47678  257prm  47685  fmtno4prmfac  47696  fmtno4nprmfac193  47698  fmtno5faclem2  47704  139prmALT  47720  127prm  47723  mod42tp1mod8  47726  3exp4mod41  47740  41prothprmlem2  47742  2exp340mod341  47857  8exp8mod9  47860  gpg5order  48184