Metamath Proof Explorer


Theorem sqge0d

Description: The square of a real is nonnegative, deduction form. (Contributed by Mario Carneiro, 28-May-2016)

Ref Expression
Hypothesis sqge0d.1 φ A
Assertion sqge0d φ 0 A 2

Proof

Step Hyp Ref Expression
1 sqge0d.1 φ A
2 sqge0 A 0 A 2
3 1 2 syl φ 0 A 2