Description: Contrapositive inference for inequality. (Contributed by NM, 18Mar2007) (Proof shortened by Andrew Salmon, 25May2011) (Proof shortened by Wolf Lammen, 22Nov2019)
Ref  Expression  

Hypothesis  necon1bi.1   ( A =/= B > ph ) 

Assertion  necon1bi   ( . ph > A = B ) 
Step  Hyp  Ref  Expression 

1  necon1bi.1   ( A =/= B > ph ) 

2  dfne   ( A =/= B <> . A = B ) 

3  2 1  sylbir   ( . A = B > ph ) 
4  3  con1i   ( . ph > A = B ) 