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 2784	1 ⊢ (𝐵 · 𝐴) = 𝐶

This proof depends on syntax axioms:   = wceq 1570   ∈ wcel 2145  (class class class)co 7412  ℂcc 11179   · cmul 11186

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-9 2155  ax-ext 2733  ax-mulcom 11245

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-cleq 2753

This theorem is used by:  divcan1i  12042  mvllmuli  12131  recgt0ii  12204  2t3e6  12490  2t4e8  12493  nummul2c  12850  5recm6rec  12945  dec5nprm  17224  karatsuba  17241  2exp11  17247  2exp16  17248  13prm  17274  17prm  17275  19prm  17276  23prm  17277  43prm  17280  83prm  17281  139prm  17282  163prm  17283  317prm  17284  631prm  17285  1259lem1  17289  1259lem2  17290  1259lem3  17291  1259lem4  17292  1259lem5  17293  1259prm  17294  2503lem1  17295  2503lem2  17296  2503lem3  17297  2503prm  17298  4001lem1  17299  4001lem2  17300  4001lem3  17301  4001lem4  17302  4001prm  17303  pcoass  25325  efif1olem2  26853  mcubic  27157  quart1  27166  quartlem1  27167  tanatan  27229  log2ublem3  27258  log2ub  27259  bclbnd  27589  bpos1lem  27591  bposlem4  27596  bposlem5  27597  bposlem8  27600  2lgsoddprmlem3c  27721  ex-exp  31033  ex-fac  31034  ex-prmo  31042  ipasslem10  31423  siii  31437  normlem3  31696  bcsiALT  31763  dpmul1000  33447  hgt750lem2  35264  12lcm5e60  43026  60lcm7e420  43028  3exp7  43071  3lexlogpow5ineq1  43072  3lexlogpow2ineq2  43077  3lexlogpow5ineq5  43078  aks4d1p1  43094  25or6to4  43224  4t5e20  43316  235t711  43330  ex-decpmul  43331  0tie0  43340  3cubeslem3r  43651  sqrtcval2  44601  resqrtvalex  44604  inductionexd  45114  fouriersw  47185  goldrasin  47873  1t10e1p1e11  48324  fmtno5lem1  48582  fmtno5lem2  48583  257prm  48590  fmtno4prmfac  48601  fmtno4nprmfac193  48603  fmtno5faclem2  48609  139prmALT  48625  127prm  48628  41prothprmlem2  48647  2exp340mod341  48775  8exp8mod9  48778  gpg5order  49102