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

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

Proof of Theorem mulcom
StepHypRef Expression
1 ax-mulcom 6985 1 ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 · 𝐵) = (𝐵 · 𝐴))
Colors of variables: wff set class
Syntax hints:  wi 4  wa 97   = wceq 1243  wcel 1393  (class class class)co 5512  cc 6887   · cmul 6894
This theorem was proved from axioms:  ax-mulcom 6985
This theorem is referenced by:  adddir  7018  mulid2  7025  mulcomi  7033  mulcomd  7048  mul12  7142  mul32  7143  mul31  7144  muladd  7381  subdir  7383  mul01  7386  mulneg2  7393  recextlem1  7632  divmulap3  7656  div23ap  7670  div13ap  7672  div12ap  7673  divcanap4  7676  divmul13ap  7691  divmul24ap  7692  divcanap7  7697  div2negap  7711  prodgt02  7819  prodge02  7821  ltmul2  7822  lemul2  7823  lemul2a  7825  ltmulgt12  7831  lemulge12  7833  ltmuldiv2  7841  ltdivmul2  7844  ledivmul2  7846  lemuldiv2  7848  times2  8039  subsq  9358  cjmulrcl  9487  imval2  9494  abscj  9650  sqabsadd  9653  sqabssub  9654
  Copyright terms: Public domain W3C validator