Description: A positive real is nonzero. (Contributed by Mario Carneiro, 28May2016)
Ref  Expression  

Hypothesis  rpred.1   ( ph > A e. RR+ ) 

Assertion  rpne0d   ( ph > A =/= 0 ) 
Step  Hyp  Ref  Expression 

1  rpred.1   ( ph > A e. RR+ ) 

2  rpne0   ( A e. RR+ > A =/= 0 ) 

3  1 2  syl   ( ph > A =/= 0 ) 