This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem divdiv3d

Description: Division into a fraction. (Contributed by Glauco Siliprandi, 24-Dec-2020)

Ref Expression
Hypotheses divdiv3d.1 ⊢ φ → A ∈ ℂ
divdiv3d.2 ⊢ φ → B ∈ ℂ
divdiv3d.3 ⊢ φ → C ∈ ℂ
divdiv3d.4 ⊢ φ → B ≠ 0
divdiv3d.5 ⊢ φ → C ≠ 0
Assertion divdiv3d ⊢ φ → A B C = A C ⁢ B

Proof

Step Hyp Ref Expression
1 divdiv3d.1 ⊢ φ → A ∈ ℂ
2 divdiv3d.2 ⊢ φ → B ∈ ℂ
3 divdiv3d.3 ⊢ φ → C ∈ ℂ
4 divdiv3d.4 ⊢ φ → B ≠ 0
5 divdiv3d.5 ⊢ φ → C ≠ 0
6 1 2 3 4 5 divdiv1d ⊢ φ → A B C = A B ⁢ C
7 2 3 mulcomd ⊢ φ → B ⁢ C = C ⁢ B
8 7 oveq2d ⊢ φ → A B ⁢ C = A C ⁢ B
9 6 8 eqtrd ⊢ φ → A B C = A C ⁢ B