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

Theorem mulcomd 7445
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 7407 . 2 ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 · 𝐵) = (𝐵 · 𝐴))
41, 2, 3syl2anc 403 1 (𝜑 → (𝐴 · 𝐵) = (𝐵 · 𝐴))
Colors of variables: wff set class
Syntax hints:  wi 4   = wceq 1287  wcel 1436  (class class class)co 5606  cc 7284   · cmul 7291
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia3 106  ax-mulcom 7382
This theorem is referenced by:  mul31  7549  remulext2  8010  mulreim  8014  mulext2  8023  mulcanapd  8061  mulcanap2d  8062  divcanap1  8079  divrecap2  8087  div23ap  8089  divdivdivap  8111  divmuleqap  8115  divadddivap  8125  divcanap5rd  8214  dmdcanap2d  8217  mvllmulapd  8231  prodgt0  8240  lt2mul2div  8267  mulle0r  8332  qapne  9048  modqvalr  9652  modqcyc  9686  mulp1mod1  9692  modqmul12d  9705  modqnegd  9706  modqmulmodr  9717  addmodlteq  9725  expaddzap  9889  binom2  9954  binom3  9959  bccmpl  10050  bcm1k  10056  bcn2  10060  bcpasc  10062  cvg1nlemcxze  10302  cvg1nlemcau  10304  resqrexlemcalc1  10334  resqrexlemcalc2  10335  resqrexlemnm  10338  recvalap  10417  nndivides  10669  dvds2ln  10695  even2n  10740  oddm1even  10741  m1exp1  10767  divalgmod  10793  mulgcdr  10873  rplpwr  10882  lcmgcdlem  10925  divgcdcoprmex  10950  cncongr1  10951  oddpwdclemxy  11013  2sqpwodd  11020  evenennn  11072
  Copyright terms: Public domain W3C validator