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

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

Proof of Theorem mulcom
StepHypRef Expression
1 ax-mulcom 7043 1 ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 · 𝐵) = (𝐵 · 𝐴))
 Colors of variables: wff set class Syntax hints:   → wi 4   ∧ wa 101   = wceq 1259   ∈ wcel 1409  (class class class)co 5540  ℂcc 6945   · cmul 6952 This theorem was proved from axioms:  ax-mulcom 7043 This theorem is referenced by:  adddir  7076  mulid2  7083  mulcomi  7091  mulcomd  7106  mul12  7203  mul32  7204  mul31  7205  muladd  7453  subdir  7455  mul01  7458  mulneg2  7465  recextlem1  7706  divmulap3  7730  div23ap  7744  div13ap  7746  div12ap  7747  divcanap4  7750  divmul13ap  7766  divmul24ap  7767  divcanap7  7772  div2negap  7786  prodgt02  7894  prodge02  7896  ltmul2  7897  lemul2  7898  lemul2a  7900  ltmulgt12  7906  lemulge12  7908  ltmuldiv2  7916  ltdivmul2  7919  ledivmul2  7921  lemuldiv2  7923  times2  8112  modqcyc2  9310  subsq  9525  cjmulrcl  9715  imval2  9722  abscj  9879  sqabsadd  9882  sqabssub  9883  dvdsmul1  10129  odd2np1lem  10183  odd2np1  10184  opeo  10209  omeo  10210
 Copyright terms: Public domain W3C validator