Theorem mulcomli 11299

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

Syntax hints:   = wceq 1537   ∈ wcel 2108  (class class class)co 7448  ℂcc 11182   · cmul 11189

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-9 2118  ax-ext 2711  ax-mulcom 11248

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1778  df-cleq 2732

This theorem is referenced by:  divcan1i  12038  mvllmuli  12127  recgt0ii  12201  nummul2c  12808  halfthird  12901  5recm6rec  12902  sq4e2t8  14248  cos2bnd  16236  prmo3  17088  dec5nprm  17113  decexp2  17122  karatsuba  17131  2exp6  17134  2exp8  17136  2exp11  17137  2exp16  17138  7prm  17158  13prm  17163  17prm  17164  19prm  17165  23prm  17166  43prm  17169  83prm  17170  139prm  17171  163prm  17172  317prm  17173  631prm  17174  1259lem1  17178  1259lem2  17179  1259lem3  17180  1259lem4  17181  1259lem5  17182  1259prm  17183  2503lem1  17184  2503lem2  17185  2503lem3  17186  2503prm  17187  4001lem1  17188  4001lem2  17189  4001lem3  17190  4001lem4  17191  4001prm  17192  pcoass  25076  efif1olem2  26603  mcubic  26908  quart1lem  26916  quart1  26917  quartlem1  26918  tanatan  26980  log2ublem3  27009  log2ub  27010  cht3  27234  bclbnd  27342  bpos1lem  27344  bposlem4  27349  bposlem5  27350  bposlem8  27353  2lgslem3a  27458  2lgsoddprmlem3c  27474  2lgsoddprmlem3d  27475  ex-exp  30482  ex-fac  30483  ex-prmo  30491  ipasslem10  30871  siii  30885  normlem3  31144  bcsiALT  31211  dpmul1000  32863  hgt750lem2  34629  12lcm5e60  41965  60lcm7e420  41967  420lcm8e840  41968  3exp7  42010  3lexlogpow5ineq1  42011  3lexlogpow2ineq2  42016  3lexlogpow5ineq5  42017  aks4d1p1  42033  4t5e20  42280  235t711  42293  ex-decpmul  42294  0tie0  42304  3cubeslem3l  42642  3cubeslem3r  42643  sqrtcval2  43604  resqrtvalex  43607  inductionexd  44117  fouriersw  46152  1t10e1p1e11  47225  fmtno5lem1  47427  fmtno5lem2  47428  257prm  47435  fmtno4prmfac  47446  fmtno4nprmfac193  47448  fmtno5faclem2  47454  139prmALT  47470  127prm  47473  mod42tp1mod8  47476  3exp4mod41  47490  41prothprmlem2  47492  2exp340mod341  47607  8exp8mod9  47610