Metamath Proof Explorer

Theorem necon3ai

Description: Contrapositive inference for inequality. (Contributed by NM, 23-May-2007) (Proof shortened by Andrew Salmon, 25-May-2011)

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

Proof

Step Hyp Ref Expression
1 necon3ai.1 
 |-  ( ph -> A = B )
2 nne 
 |-  ( -. A =/= B <-> A = B )
3 1 2 sylibr 
 |-  ( ph -> -. A =/= B )
4 3 con2i 
 |-  ( A =/= B -> -. ph )