Metamath Proof Explorer

Theorem neneq

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

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

Proof

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