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

Metamath Proof Explorer

Theorem redivcld

Description: Closure law for division of reals. (Contributed by Mario Carneiro, 27-May-2016)

Ref Expression
Hypotheses redivcld.1 ⊢ φ → A ∈ ℝ
redivcld.2 ⊢ φ → B ∈ ℝ
redivcld.3 ⊢ φ → B ≠ 0
Assertion redivcld ⊢ φ → A B ∈ ℝ

Proof

Step Hyp Ref Expression
1 redivcld.1 ⊢ φ → A ∈ ℝ
2 redivcld.2 ⊢ φ → B ∈ ℝ
3 redivcld.3 ⊢ φ → B ≠ 0
4 redivcl ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ B ≠ 0 → A B ∈ ℝ
5 1 2 3 4 syl3anc ⊢ φ → A B ∈ ℝ