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

Theorem mulcomd 7810
Description: Commutative law for multiplication. (Contributed by Mario Carneiro, 27-May-2016.)
Hypotheses
Ref Expression
addcld.1 (𝜑𝐴 ∈ ℂ)
addcld.2 (𝜑𝐵 ∈ ℂ)
Assertion
Ref Expression
mulcomd (𝜑 → (𝐴 · 𝐵) = (𝐵 · 𝐴))

Proof of Theorem mulcomd
StepHypRef Expression
1 addcld.1 . 2 (𝜑𝐴 ∈ ℂ)
2 addcld.2 . 2 (𝜑𝐵 ∈ ℂ)
3 mulcom 7772 . 2 ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 · 𝐵) = (𝐵 · 𝐴))
41, 2, 3syl2anc 409 1 (𝜑 → (𝐴 · 𝐵) = (𝐵 · 𝐴))
Colors of variables: wff set class
Syntax hints:  wi 4   = wceq 1332  wcel 1481  (class class class)co 5781  cc 7641   · cmul 7648
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia3 107  ax-mulcom 7744
This theorem is referenced by:  mul31  7916  remulext2  8385  mulreim  8389  mulext2  8398  mulcanapd  8445  mulcanap2d  8446  divcanap1  8464  divrecap2  8472  div23ap  8474  divdivdivap  8496  divmuleqap  8500  divadddivap  8510  apmul2  8572  apdivmuld  8596  divcanap5rd  8601  dmdcanap2d  8604  mvllmulapd  8624  prodgt0  8633  lt2mul2div  8660  mulle0r  8725  qapne  9457  mul2lt0llt0  9577  mul2lt0lgt0  9578  mul2lt0pn  9580  modqvalr  10128  modqcyc  10162  mulp1mod1  10168  modqmul12d  10181  modqnegd  10182  modqmulmodr  10193  addmodlteq  10201  expaddzap  10367  binom2  10433  binom3  10439  bccmpl  10531  bcm1k  10537  bcn2  10541  bcpasc  10543  cvg1nlemcxze  10785  cvg1nlemcau  10787  resqrexlemcalc1  10817  resqrexlemcalc2  10818  resqrexlemnm  10821  recvalap  10900  bdtrilem  11041  reccn2ap  11113  isummulc1  11227  fsummulc1  11249  trireciplem  11300  geolim  11311  cvgratnnlemnexp  11324  cvgratnnlemmn  11325  cvgratnnlemfm  11329  cvgratz  11332  mertensabs  11337  eftlub  11431  sinadd  11477  cosadd  11478  sin2t  11490  nndivides  11534  dvds2ln  11560  even2n  11605  oddm1even  11606  m1exp1  11632  divalgmod  11658  mulgcdr  11740  rplpwr  11749  lcmgcdlem  11792  divgcdcoprmex  11817  cncongr1  11818  oddpwdclemxy  11881  2sqpwodd  11888  evenennn  11940  dvmulxxbr  12872  dvmptcmulcn  12889  tangtx  12965  cxpmul  13039  abscxp  13041
  Copyright terms: Public domain W3C validator