Metamath Proof Explorer


Theorem sq0id

Description: If a number is zero, then its square is zero. Deduction form of sq0i . Converse of sqeq0d . (Contributed by David Moews, 28-Feb-2017)

Ref Expression
Hypothesis sq0id.1 ⊢ φ → A = 0
Assertion sq0id ⊢ φ → A 2 = 0

Proof

Step Hyp Ref Expression
1 sq0id.1 ⊢ φ → A = 0
2 sq0i ⊢ A = 0 → A 2 = 0
3 1 2 syl ⊢ φ → A 2 = 0