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

Step	Hyp	Ref	Expression
1		addcld.1	. 2 ⊢ (φ → A ∈ ℂ)
2		addcld.2	. 2 ⊢ (φ → B ∈ ℂ)
3		mulcom 6808	. 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 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