Metamath Proof Explorer


Theorem resqcld

Description: Closure of squaring in reals, deduction form. (Contributed by Mario Carneiro, 28-May-2016)

Ref Expression
Hypothesis resqcld.1 ⊢ φ → A ∈ ℝ
Assertion resqcld ⊢ φ → A 2 ∈ ℝ

Proof

Step Hyp Ref Expression
1 resqcld.1 ⊢ φ → A ∈ ℝ
2 resqcl ⊢ A ∈ ℝ → A 2 ∈ ℝ
3 1 2 syl ⊢ φ → A 2 ∈ ℝ