ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  mulcom GIF version

Theorem mulcom 7407
Description: Alias for ax-mulcom 7382, for naming consistency with mulcomi 7430. (Contributed by NM, 10-Mar-2008.)
Assertion
Ref Expression
mulcom ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 · 𝐵) = (𝐵 · 𝐴))

Proof of Theorem mulcom
StepHypRef Expression
1 ax-mulcom 7382 1 ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 · 𝐵) = (𝐵 · 𝐴))
Colors of variables: wff set class
Syntax hints:  wi 4  wa 102   = wceq 1287  wcel 1436  (class class class)co 5606  cc 7284   · cmul 7291
This theorem was proved from axioms:  ax-mulcom 7382
This theorem is referenced by:  adddir  7415  mulid2  7422  mulcomi  7430  mulcomd  7445  mul12  7547  mul32  7548  mul31  7549  muladd  7798  subdir  7800  mul01  7803  mulneg2  7810  recextlem1  8051  divmulap3  8075  div23ap  8089  div13ap  8091  div12ap  8092  divmulasscomap  8094  divcanap4  8097  divmul13ap  8113  divmul24ap  8114  divcanap7  8119  div2negap  8133  prodgt02  8241  prodge02  8243  ltmul2  8244  lemul2  8245  lemul2a  8247  ltmulgt12  8253  lemulge12  8255  ltmuldiv2  8263  ltdivmul2  8266  ledivmul2  8268  lemuldiv2  8270  times2  8471  modqcyc2  9687  subsq  9950  cjmulrcl  10208  imval2  10215  abscj  10372  sqabsadd  10375  sqabssub  10376  dvdsmul1  10684  odd2np1lem  10738  odd2np1  10739  opeo  10763  omeo  10764  modgcd  10848  dvdsgcd  10867  gcdmultiple  10875  coprmdvds  10940  coprmdvds2  10941  qredeq  10944
  Copyright terms: Public domain W3C validator