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

Theorem mulcomd 7755
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 7717 . 2 ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 · 𝐵) = (𝐵 · 𝐴))
41, 2, 3syl2anc 408 1 (𝜑 → (𝐴 · 𝐵) = (𝐵 · 𝐴))
Colors of variables: wff set class
Syntax hints:  wi 4   = wceq 1316  wcel 1465  (class class class)co 5742  cc 7586   · cmul 7593
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia3 107  ax-mulcom 7689
This theorem is referenced by:  mul31  7861  remulext2  8330  mulreim  8334  mulext2  8343  mulcanapd  8390  mulcanap2d  8391  divcanap1  8409  divrecap2  8417  div23ap  8419  divdivdivap  8441  divmuleqap  8445  divadddivap  8455  apmul2  8517  apdivmuld  8541  divcanap5rd  8546  dmdcanap2d  8549  mvllmulapd  8569  prodgt0  8578  lt2mul2div  8605  mulle0r  8670  qapne  9399  mul2lt0llt0  9516  mul2lt0lgt0  9517  mul2lt0pn  9519  modqvalr  10066  modqcyc  10100  mulp1mod1  10106  modqmul12d  10119  modqnegd  10120  modqmulmodr  10131  addmodlteq  10139  expaddzap  10305  binom2  10371  binom3  10377  bccmpl  10468  bcm1k  10474  bcn2  10478  bcpasc  10480  cvg1nlemcxze  10722  cvg1nlemcau  10724  resqrexlemcalc1  10754  resqrexlemcalc2  10755  resqrexlemnm  10758  recvalap  10837  bdtrilem  10978  reccn2ap  11050  isummulc1  11164  fsummulc1  11186  trireciplem  11237  geolim  11248  cvgratnnlemnexp  11261  cvgratnnlemmn  11262  cvgratnnlemfm  11266  cvgratz  11269  mertensabs  11274  eftlub  11323  sinadd  11370  cosadd  11371  sin2t  11383  nndivides  11427  dvds2ln  11453  even2n  11498  oddm1even  11499  m1exp1  11525  divalgmod  11551  mulgcdr  11633  rplpwr  11642  lcmgcdlem  11685  divgcdcoprmex  11710  cncongr1  11711  oddpwdclemxy  11774  2sqpwodd  11781  evenennn  11833  dvmulxxbr  12762  dvmptcmulcn  12779  tangtx  12846
  Copyright terms: Public domain W3C validator