Theorem gt0ne0d

Description: Positive implies nonzero. (Contributed by Mario Carneiro, 27-May-2016)

	Ref	Expression
Hypothesis	gt0ne0d.1	⊢ ( 𝜑 → 0 < 𝐴 )
Assertion	gt0ne0d	⊢ ( 𝜑 → 𝐴 ≠ 0 )

Proof

Step	Hyp	Ref	Expression
1		gt0ne0d.1	⊢ ( 𝜑 → 0 < 𝐴 )
2		0red	⊢ ( 𝜑 → 0 ∈ ℝ )
3	2 1	gtned	⊢ ( 𝜑 → 𝐴 ≠ 0 )