Description: Infer an equivalence from an implication and its converse. Inference associated with impbi . (Contributed by NM, 29Dec1992)
Ref  Expression  

Hypotheses  impbii.1   ( ph > ps ) 

impbii.2   ( ps > ph ) 

Assertion  impbii   ( ph <> ps ) 
Step  Hyp  Ref  Expression 

1  impbii.1   ( ph > ps ) 

2  impbii.2   ( ps > ph ) 

3  impbi   ( ( ph > ps ) > ( ( ps > ph ) > ( ph <> ps ) ) ) 

4  1 2 3  mp2   ( ph <> ps ) 