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

Step	Hyp	Ref	Expression
1		addcld.1	. 2 ⊢ (φ → A ∈ ℂ)
2		addcld.2	. 2 ⊢ (φ → B ∈ ℂ)
3		mulcom 6768	. 2 ⊢ ((A ∈ ℂ ∧ B ∈ ℂ) → (A · B) = (B · A))
4	1, 2, 3	syl2anc 391	1 ⊢ (φ → (A · B) = (B · A))

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