Theorem sqr00d

Description: A square root is zero iff its argument is 0. (Contributed by Mario Carneiro, 29-May-2016)

	Ref	Expression
Hypotheses	abscld.1	$$⊢\phi \to A\in ℂ$$
	sqrt00d.2	$$⊢\phi \to \sqrt{A}=0$$
Assertion	sqr00d	$$⊢\phi \to A=0$$

Proof

Step	Hyp	Ref	Expression
1		abscld.1	$$⊢\phi \to A\in ℂ$$
2		sqrt00d.2	$$⊢\phi \to \sqrt{A}=0$$
3	1	sqsqrtd	$$⊢\phi \to {\sqrt{A}}^2=A$$
4	2	sq0id	$$⊢\phi \to {\sqrt{A}}^2=0$$
5	3 4	eqtr3d	$$⊢\phi \to A=0$$