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

Theorem mulcomd 7191
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 7153 . 2 ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 · 𝐵) = (𝐵 · 𝐴))
41, 2, 3syl2anc 403 1 (𝜑 → (𝐴 · 𝐵) = (𝐵 · 𝐴))
Colors of variables: wff set class
Syntax hints:  wi 4   = wceq 1285  wcel 1434  (class class class)co 5537  cc 7030   · cmul 7037
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia3 106  ax-mulcom 7128
This theorem is referenced by:  mul31  7295  remulext2  7756  mulreim  7760  mulext2  7769  mulcanapd  7807  mulcanap2d  7808  divcanap1  7825  divrecap2  7833  div23ap  7835  divdivdivap  7857  divmuleqap  7861  divadddivap  7871  divcanap5rd  7960  dmdcanap2d  7963  mvllmulapd  7977  prodgt0  7986  lt2mul2div  8013  mulle0r  8078  qapne  8794  modqvalr  9396  modqcyc  9430  mulp1mod1  9436  modqmul12d  9449  modqnegd  9450  modqmulmodr  9461  addmodlteq  9469  expaddzap  9606  binom2  9671  binom3  9676  bccmpl  9767  bcm1k  9773  bcn2  9777  bcpasc  9779  cvg1nlemcxze  9995  cvg1nlemcau  9997  resqrexlemcalc1  10027  resqrexlemcalc2  10028  resqrexlemnm  10031  recvalap  10110  nndivides  10336  dvds2ln  10362  even2n  10407  oddm1even  10408  m1exp1  10434  divalgmod  10460  mulgcdr  10540  rplpwr  10549  lcmgcdlem  10592  divgcdcoprmex  10617  cncongr1  10618  oddpwdclemxy  10680  2sqpwodd  10687
  Copyright terms: Public domain W3C validator