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

Theorem mulcomd 6806
Description: Commutative law for multiplication. (Contributed by Mario Carneiro, 27-May-2016.)
Hypotheses
Ref Expression
addcld.1 (φA ℂ)
addcld.2 (φB ℂ)
Assertion
Ref Expression
mulcomd (φ → (A · B) = (B · A))

Proof of Theorem mulcomd
StepHypRef Expression
1 addcld.1 . 2 (φA ℂ)
2 addcld.2 . 2 (φB ℂ)
3 mulcom 6768 . 2 ((A B ℂ) → (A · B) = (B · A))
41, 2, 3syl2anc 391 1 (φ → (A · B) = (B · A))
Colors of variables: wff set class
Syntax hints:  wi 4   = wceq 1242   wcel 1390  (class class class)co 5455  cc 6669   · cmul 6676
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia3 101  ax-mulcom 6744
This theorem is referenced by:  mul31  6901  remulext2  7344  mulreim  7348  mulext2  7357  mulcanapd  7384  mulcanap2d  7385  divcanap1  7402  divrecap2  7410  div23ap  7412  divdivdivap  7431  divmuleqap  7435  divadddivap  7445  divcanap5rd  7534  dmdcanap2d  7537  mvllmulapd  7550  prodgt0  7559  lt2mul2div  7586  qapne  8310  expaddzap  8913  binom2  8975  binom3  8979
  Copyright terms: Public domain W3C validator