Metamath Proof Explorer


Theorem sq0id

Description: If a number is zero, 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