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 ∈ ℂ → A B ⁢ C = A ⁢ C B

Proof

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