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

Theorem mulcomd 7046
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 7008 . 2 ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 · 𝐵) = (𝐵 · 𝐴))
41, 2, 3syl2anc 391 1 (𝜑 → (𝐴 · 𝐵) = (𝐵 · 𝐴))
Colors of variables: wff set class
Syntax hints:  wi 4   = wceq 1243  wcel 1393  (class class class)co 5512  cc 6885   · cmul 6892
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia3 101  ax-mulcom 6983
This theorem is referenced by:  mul31  7142  remulext2  7589  mulreim  7593  mulext2  7602  mulcanapd  7640  mulcanap2d  7641  divcanap1  7658  divrecap2  7666  div23ap  7668  divdivdivap  7687  divmuleqap  7691  divadddivap  7701  divcanap5rd  7790  dmdcanap2d  7793  mvllmulapd  7807  prodgt0  7816  lt2mul2div  7843  qapne  8572  modqvalr  9165  expaddzap  9297  binom2  9360  binom3  9364  cvg1nlemcxze  9579  cvg1nlemcau  9581  resqrexlemcalc1  9610  resqrexlemcalc2  9611  resqrexlemnm  9614  recvalap  9691
  Copyright terms: Public domain W3C validator