Theorem mulcomli 11206

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

Syntax hints:   = wceq 1563   ∈ wcel 2145  (class class class)co 7400  ℂcc 11086   · cmul 11093

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1818  ax-4 1832  ax-5 1933  ax-6 1990  ax-7 2031  ax-9 2155  ax-ext 2737  ax-mulcom 11152

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1803  df-cleq 2757

This theorem is referenced by:  divcan1i  11950  mvllmuli  12039  recgt0ii  12112  2t3e6  12398  2t4e8  12401  halfthird  12456  nummul2c  12757  5recm6rec  12852  sq4e2t8  14226  cos2bnd  16234  prmo3  17091  dec5nprm  17116  karatsuba  17133  2exp6  17136  2exp8  17138  2exp11  17139  2exp16  17140  7prm  17160  13prm  17166  17prm  17167  19prm  17168  23prm  17169  43prm  17172  83prm  17173  139prm  17174  163prm  17175  317prm  17176  631prm  17177  1259lem1  17181  1259lem2  17182  1259lem3  17183  1259lem4  17184  1259lem5  17185  1259prm  17186  2503lem1  17187  2503lem2  17188  2503lem3  17189  2503prm  17190  4001lem1  17191  4001lem2  17192  4001lem3  17193  4001lem4  17194  4001prm  17195  pcoass  25144  efif1olem2  26666  mcubic  26970  quart1lem  26978  quart1  26979  quartlem1  26980  tanatan  27042  log2ublem3  27071  log2ub  27072  bclbnd  27402  bpos1lem  27404  bposlem4  27409  bposlem5  27410  bposlem8  27413  2lgslem3a  27518  2lgsoddprmlem3c  27534  2lgsoddprmlem3d  27535  ex-exp  30710  ex-fac  30711  ex-prmo  30719  ipasslem10  31100  siii  31114  normlem3  31373  bcsiALT  31440  dpmul1000  33131  hgt750lem2  34956  12lcm5e60  42637  60lcm7e420  42639  420lcm8e840  42640  3exp7  42682  3lexlogpow5ineq1  42683  3lexlogpow2ineq2  42688  3lexlogpow5ineq5  42689  aks4d1p1  42705  4t5e20  42912  235t711  42926  ex-decpmul  42927  0tie0  42936  3cubeslem3l  43279  3cubeslem3r  43280  sqrtcval2  44230  resqrtvalex  44233  inductionexd  44743  fouriersw  46803  goldrasin  47474  1t10e1p1e11  47902  fmtno5lem1  48160  fmtno5lem2  48161  257prm  48168  fmtno4prmfac  48179  fmtno4nprmfac193  48181  fmtno5faclem2  48187  139prmALT  48203  127prm  48206  3exp4mod41  48223  41prothprmlem2  48225  2exp340mod341  48353  8exp8mod9  48356  gpg5order  48680