Metamath Proof Explorer


Theorem absne0d

Description: The absolute value of a number is zero iff the number is zero. Proposition 10-3.7(c) of Gleason p. 133. (Contributed by Mario Carneiro, 29-May-2016)

Ref Expression
Hypotheses abscld.1 φA
absne0d.2 φA0
Assertion absne0d φA0

Proof

Step Hyp Ref Expression
1 abscld.1 φA
2 absne0d.2 φA0
3 1 abs00ad φA=0A=0
4 3 necon3bid φA0A0
5 2 4 mpbird φA0