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

Theorem mulcomd 6846
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 6808 . 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 6709   · cmul 6716
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia3 101  ax-mulcom 6784
This theorem is referenced by:  mul31  6941  remulext2  7384  mulreim  7388  mulext2  7397  mulcanapd  7424  mulcanap2d  7425  divcanap1  7442  divrecap2  7450  div23ap  7452  divdivdivap  7471  divmuleqap  7475  divadddivap  7485  divcanap5rd  7574  dmdcanap2d  7577  mvllmulapd  7590  prodgt0  7599  lt2mul2div  7626  qapne  8350  expaddzap  8953  binom2  9015  binom3  9019
  Copyright terms: Public domain W3C validator