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

Theorem mulcom 7971
Description: Alias for ax-mulcom 7943, for naming consistency with mulcomi 7994. (Contributed by NM, 10-Mar-2008.)
Assertion
Ref Expression
mulcom  |-  ( ( A  e.  CC  /\  B  e.  CC )  ->  ( A  x.  B
)  =  ( B  x.  A ) )

Proof of Theorem mulcom
StepHypRef Expression
1 ax-mulcom 7943 1  |-  ( ( A  e.  CC  /\  B  e.  CC )  ->  ( A  x.  B
)  =  ( B  x.  A ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 104    = wceq 1364    e. wcel 2160  (class class class)co 5897   CCcc 7840    x. cmul 7847
This theorem was proved from axioms:  ax-mulcom 7943
This theorem is referenced by:  adddir  7979  mullid  7986  mulcomi  7994  mulcomd  8010  mul12  8117  mul32  8118  mul31  8119  muladd  8372  subdir  8374  mul01  8377  mulneg2  8384  recextlem1  8639  divmulap3  8665  div23ap  8679  div13ap  8681  div12ap  8682  divmulasscomap  8684  divcanap4  8687  divmul13ap  8703  divmul24ap  8704  divcanap7  8709  div2negap  8723  prodgt02  8841  prodge02  8843  ltmul2  8844  lemul2  8845  lemul2a  8847  ltmulgt12  8853  lemulge12  8855  ltmuldiv2  8863  ltdivmul2  8866  ledivmul2  8868  lemuldiv2  8870  times2  9079  modqcyc2  10393  subsq  10661  cjmulrcl  10931  imval2  10938  abscj  11096  sqabsadd  11099  sqabssub  11100  prod3fmul  11584  prodmodclem3  11618  efcllemp  11701  efexp  11725  sinmul  11787  demoivreALT  11816  dvdsmul1  11855  odd2np1lem  11912  odd2np1  11913  opeo  11937  omeo  11938  modgcd  12027  dvdsgcd  12048  gcdmultiple  12056  coprmdvds  12127  coprmdvds2  12128  qredeq  12131  modprm0  12289  modprmn0modprm0  12291  coprimeprodsq2  12293  cncrng  13889  ef2kpi  14704  sinperlem  14706  sinmpi  14713  cosmpi  14714  sinppi  14715  cosppi  14716  cxpcom  14834  lgsdir2lem4  14910  lgsdir2  14912
  Copyright terms: Public domain W3C validator