Theorem neneq 2800

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

Assertion

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

Proof of Theorem neneq

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

Syntax hints:   -. wn 3   -> wi 4   = wceq 1483   =/= wne 2794

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 197  df-ne 2795

This theorem is referenced by:  necon3ad  2807  nelsnOLD  4213  pr1eqbg  4390  fpropnf1  6524  mpt2difsnif  6753  hash2prd  13257  fprodn0f  14722  gcd2n0cl  15231  lcmfunsnlem2lem1  15351  isnsgrp  17288  isnmnd  17298  structiedg0val  25911  umgr2edgneu  26106  clwwlknclwwlkdifs  26873  numclwwlk3lem  27241  n0p  39209  supxrge  39554  uzn0bi  39689  elprn1  39865  elprn2  39866  itgcoscmulx  40185  fourierdlem41  40365  elaa2  40451  sge0cl  40598  meadjiunlem  40682  hoidmvlelem2  40810  hspmbllem1  40840  2reu4a  41189  fdmdifeqresdif  42120