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

Theorem mulcom 7763
Description: Alias for ax-mulcom 7735, for naming consistency with mulcomi 7786. (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 7735 1  |-  ( ( A  e.  CC  /\  B  e.  CC )  ->  ( A  x.  B
)  =  ( B  x.  A ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 103    = wceq 1331    e. wcel 1480  (class class class)co 5774   CCcc 7632    x. cmul 7639
This theorem was proved from axioms:  ax-mulcom 7735
This theorem is referenced by:  adddir  7771  mulid2  7778  mulcomi  7786  mulcomd  7801  mul12  7905  mul32  7906  mul31  7907  muladd  8160  subdir  8162  mul01  8165  mulneg2  8172  recextlem1  8426  divmulap3  8451  div23ap  8465  div13ap  8467  div12ap  8468  divmulasscomap  8470  divcanap4  8473  divmul13ap  8489  divmul24ap  8490  divcanap7  8495  div2negap  8509  prodgt02  8625  prodge02  8627  ltmul2  8628  lemul2  8629  lemul2a  8631  ltmulgt12  8637  lemulge12  8639  ltmuldiv2  8647  ltdivmul2  8650  ledivmul2  8652  lemuldiv2  8654  times2  8863  modqcyc2  10147  subsq  10413  cjmulrcl  10673  imval2  10680  abscj  10838  sqabsadd  10841  sqabssub  10842  prod3fmul  11324  prodmodclem3  11358  efcllemp  11378  efexp  11402  sinmul  11464  demoivreALT  11493  dvdsmul1  11528  odd2np1lem  11582  odd2np1  11583  opeo  11607  omeo  11608  modgcd  11692  dvdsgcd  11713  gcdmultiple  11721  coprmdvds  11786  coprmdvds2  11787  qredeq  11790  ef2kpi  12911  sinperlem  12913  sinmpi  12920  cosmpi  12921  sinppi  12922  cosppi  12923  cxpcom  13038
  Copyright terms: Public domain W3C validator