Metamath Proof Explorer

Theorem neqne

Description: From non-equality to inequality. (Contributed by Glauco Siliprandi, 11-Dec-2019)

Ref Expression
Assertion neqne 
|- ( -. A = B -> A =/= B )

Proof

Step Hyp Ref Expression
1 id 
 |-  ( -. A = B -> -. A = B )
2 1 neqned 
 |-  ( -. A = B -> A =/= B )