Theorem mulcomli 11190

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

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

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 2702  ax-mulcom 11139

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

This theorem is referenced by:  divcan1i  11933  mvllmuli  12022  recgt0ii  12096  halfthird  12410  nummul2c  12706  5recm6rec  12799  sq4e2t8  14171  cos2bnd  16163  prmo3  17019  dec5nprm  17044  karatsuba  17061  2exp6  17064  2exp8  17066  2exp11  17067  2exp16  17068  7prm  17088  13prm  17093  17prm  17094  19prm  17095  23prm  17096  43prm  17099  83prm  17100  139prm  17101  163prm  17102  317prm  17103  631prm  17104  1259lem1  17108  1259lem2  17109  1259lem3  17110  1259lem4  17111  1259lem5  17112  1259prm  17113  2503lem1  17114  2503lem2  17115  2503lem3  17116  2503prm  17117  4001lem1  17118  4001lem2  17119  4001lem3  17120  4001lem4  17121  4001prm  17122  pcoass  24931  efif1olem2  26459  mcubic  26764  quart1lem  26772  quart1  26773  quartlem1  26774  tanatan  26836  log2ublem3  26865  log2ub  26866  cht3  27090  bclbnd  27198  bpos1lem  27200  bposlem4  27205  bposlem5  27206  bposlem8  27209  2lgslem3a  27314  2lgsoddprmlem3c  27330  2lgsoddprmlem3d  27331  ex-exp  30386  ex-fac  30387  ex-prmo  30395  ipasslem10  30775  siii  30789  normlem3  31048  bcsiALT  31115  dpmul1000  32826  hgt750lem2  34650  12lcm5e60  42003  60lcm7e420  42005  420lcm8e840  42006  3exp7  42048  3lexlogpow5ineq1  42049  3lexlogpow2ineq2  42054  3lexlogpow5ineq5  42055  aks4d1p1  42071  4t5e20  42286  235t711  42300  ex-decpmul  42301  0tie0  42310  3cubeslem3l  42681  3cubeslem3r  42682  sqrtcval2  43638  resqrtvalex  43641  inductionexd  44151  fouriersw  46236  1t10e1p1e11  47315  fmtno5lem1  47558  fmtno5lem2  47559  257prm  47566  fmtno4prmfac  47577  fmtno4nprmfac193  47579  fmtno5faclem2  47585  139prmALT  47601  127prm  47604  mod42tp1mod8  47607  3exp4mod41  47621  41prothprmlem2  47623  2exp340mod341  47738  8exp8mod9  47741  gpg5order  48055