Description: Infer an implication from a logical equivalence. Inference associated with biimp . (Contributed by NM, 29Dec1992)
Ref  Expression  

Hypothesis  biimpi.1   ( ph <> ps ) 

Assertion  biimpi   ( ph > ps ) 
Step  Hyp  Ref  Expression 

1  biimpi.1   ( ph <> ps ) 

2  biimp   ( ( ph <> ps ) > ( ph > ps ) ) 

3  1 2  axmp   ( ph > ps ) 