Metamath Proof Explorer

Theorem div32

Description: A commutative/associative law for division. (Contributed by Mario Carneiro, 27-May-2016)

Ref Expression
Assertion div32 ⊢A∈ℂ∧B∈ℂ∧B≠0∧C∈ℂ→AB⁢C=A⁢CB

Proof

Step Hyp Ref Expression
1 div23 ⊢A∈ℂ∧C∈ℂ∧B∈ℂ∧B≠0→A⁢CB=AB⁢C
2 divass ⊢A∈ℂ∧C∈ℂ∧B∈ℂ∧B≠0→A⁢CB=A⁢CB
3 1 2 eqtr3d ⊢A∈ℂ∧C∈ℂ∧B∈ℂ∧B≠0→AB⁢C=A⁢CB
4 3 3com23 ⊢A∈ℂ∧B∈ℂ∧B≠0∧C∈ℂ→AB⁢C=A⁢CB