Metamath Proof Explorer


Theorem ne0gt0d

Description: A nonzero nonnegative number is positive. (Contributed by Mario Carneiro, 27-May-2016)

Ref Expression
Hypotheses ltd.1 φ A
ne0gt0d.2 φ 0 A
ne0gt0d.3 φ A 0
Assertion ne0gt0d φ 0 < A

Proof

Step Hyp Ref Expression
1 ltd.1 φ A
2 ne0gt0d.2 φ 0 A
3 ne0gt0d.3 φ A 0
4 ne0gt0 A 0 A A 0 0 < A
5 1 2 4 syl2anc φ A 0 0 < A
6 3 5 mpbid φ 0 < A