Description: Inference converting an implication to a biconditional with conjunction. Inference from Theorem *4.71 of WhiteheadRussell p. 120 (with conjunct reversed). (Contributed by NM, 1Dec2003)
Ref  Expression  

Hypothesis  pm4.71ri.1   ( ph > ps ) 

Assertion  pm4.71ri   ( ph <> ( ps /\ ph ) ) 
Step  Hyp  Ref  Expression 

1  pm4.71ri.1   ( ph > ps ) 

2  1  pm4.71i   ( ph <> ( ph /\ ps ) ) 
3  2  biancomi   ( ph <> ( ps /\ ph ) ) 