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 φA2=0

Proof

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