Theorem mulcomli 11183

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

Syntax hints:   = wceq 1540   ∈ wcel 2109  (class class class)co 7387  ℂcc 11066   · cmul 11073

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-9 2119  ax-ext 2701  ax-mulcom 11132

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-cleq 2721

This theorem is referenced by:  divcan1i  11926  mvllmuli  12015  recgt0ii  12089  halfthird  12403  nummul2c  12699  5recm6rec  12792  sq4e2t8  14164  cos2bnd  16156  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  24924  efif1olem2  26452  mcubic  26757  quart1lem  26765  quart1  26766  quartlem1  26767  tanatan  26829  log2ublem3  26858  log2ub  26859  cht3  27083  bclbnd  27191  bpos1lem  27193  bposlem4  27198  bposlem5  27199  bposlem8  27202  2lgslem3a  27307  2lgsoddprmlem3c  27323  2lgsoddprmlem3d  27324  ex-exp  30379  ex-fac  30380  ex-prmo  30388  ipasslem10  30768  siii  30782  normlem3  31041  bcsiALT  31108  dpmul1000  32819  hgt750lem2  34643  12lcm5e60  41996  60lcm7e420  41998  420lcm8e840  41999  3exp7  42041  3lexlogpow5ineq1  42042  3lexlogpow2ineq2  42047  3lexlogpow5ineq5  42048  aks4d1p1  42064  4t5e20  42279  235t711  42293  ex-decpmul  42294  0tie0  42303  3cubeslem3l  42674  3cubeslem3r  42675  sqrtcval2  43631  resqrtvalex  43634  inductionexd  44144  fouriersw  46229  1t10e1p1e11  47311  fmtno5lem1  47554  fmtno5lem2  47555  257prm  47562  fmtno4prmfac  47573  fmtno4nprmfac193  47575  fmtno5faclem2  47581  139prmALT  47597  127prm  47600  mod42tp1mod8  47603  3exp4mod41  47617  41prothprmlem2  47619  2exp340mod341  47734  8exp8mod9  47737  gpg5order  48051