Theorem mulcomli 11219

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

Syntax hints:   = wceq 1570   ∈ wcel 2143  (class class class)co 7412  ℂcc 11099   · cmul 11106

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-9 2153  ax-ext 2735  ax-mulcom 11165

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1810  df-cleq 2755

This theorem is referenced by:  divcan1i  11960  mvllmuli  12049  recgt0ii  12122  2t3e6  12408  2t4e8  12411  nummul2c  12767  5recm6rec  12862  sq4e2t8  14237  cos2bnd  16245  dec5nprm  17127  karatsuba  17144  2exp8  17149  2exp11  17150  2exp16  17151  13prm  17177  17prm  17178  19prm  17179  23prm  17180  43prm  17183  83prm  17184  139prm  17185  163prm  17186  317prm  17187  631prm  17188  1259lem1  17192  1259lem2  17193  1259lem3  17194  1259lem4  17195  1259lem5  17196  1259prm  17197  2503lem1  17198  2503lem2  17199  2503lem3  17200  2503prm  17201  4001lem1  17202  4001lem2  17203  4001lem3  17204  4001lem4  17205  4001prm  17206  pcoass  25164  efif1olem2  26686  mcubic  26990  quart1lem  26998  quart1  26999  quartlem1  27000  tanatan  27062  log2ublem3  27091  log2ub  27092  bclbnd  27422  bpos1lem  27424  bposlem4  27429  bposlem5  27430  bposlem8  27433  2lgslem3a  27538  2lgsoddprmlem3c  27554  2lgsoddprmlem3d  27555  ex-exp  30779  ex-fac  30780  ex-prmo  30788  ipasslem10  31169  siii  31183  normlem3  31442  bcsiALT  31509  dpmul1000  33196  hgt750lem2  35017  12lcm5e60  42753  60lcm7e420  42755  420lcm8e840  42756  3exp7  42798  3lexlogpow5ineq1  42799  3lexlogpow2ineq2  42804  3lexlogpow5ineq5  42805  aks4d1p1  42821  25or6to4  42951  4t5e20  43030  235t711  43044  ex-decpmul  43045  0tie0  43054  3cubeslem3l  43397  3cubeslem3r  43398  sqrtcval2  44348  resqrtvalex  44351  inductionexd  44861  fouriersw  46925  goldrasin  47596  1t10e1p1e11  48024  fmtno5lem1  48282  fmtno5lem2  48283  257prm  48290  fmtno4prmfac  48301  fmtno4nprmfac193  48303  fmtno5faclem2  48309  139prmALT  48325  127prm  48328  3exp4mod41  48345  41prothprmlem2  48347  2exp340mod341  48475  8exp8mod9  48478  gpg5order  48802