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

Theorem mulcom 7164
Description: Alias for ax-mulcom 7139, for naming consistency with mulcomi 7187. (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 7139 1  |-  ( ( A  e.  CC  /\  B  e.  CC )  ->  ( A  x.  B
)  =  ( B  x.  A ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 102    = wceq 1285    e. wcel 1434  (class class class)co 5543   CCcc 7041    x. cmul 7048
This theorem was proved from axioms:  ax-mulcom 7139
This theorem is referenced by:  adddir  7172  mulid2  7179  mulcomi  7187  mulcomd  7202  mul12  7304  mul32  7305  mul31  7306  muladd  7555  subdir  7557  mul01  7560  mulneg2  7567  recextlem1  7808  divmulap3  7832  div23ap  7846  div13ap  7848  div12ap  7849  divmulasscomap  7851  divcanap4  7854  divmul13ap  7870  divmul24ap  7871  divcanap7  7876  div2negap  7890  prodgt02  7998  prodge02  8000  ltmul2  8001  lemul2  8002  lemul2a  8004  ltmulgt12  8010  lemulge12  8012  ltmuldiv2  8020  ltdivmul2  8023  ledivmul2  8025  lemuldiv2  8027  times2  8228  modqcyc2  9442  subsq  9678  cjmulrcl  9912  imval2  9919  abscj  10076  sqabsadd  10079  sqabssub  10080  dvdsmul1  10362  odd2np1lem  10416  odd2np1  10417  opeo  10441  omeo  10442  modgcd  10526  dvdsgcd  10545  gcdmultiple  10553  coprmdvds  10618  coprmdvds2  10619  qredeq  10622
  Copyright terms: Public domain W3C validator