Metamath Proof Explorer

Theorem necon2bi

Description: Contrapositive inference for inequality. (Contributed by NM, 1-Apr-2007)

Ref Expression
Hypothesis necon2bi.1 
|- ( ph -> A =/= B )
Assertion necon2bi 
|- ( A = B -> -. ph )

Proof

Step Hyp Ref Expression
1 necon2bi.1 
 |-  ( ph -> A =/= B )
2 1 neneqd 
 |-  ( ph -> -. A = B )
3 2 con2i 
 |-  ( A = B -> -. ph )