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 )