Theorem neqned 2410

Description: If it is not the case that two classes are equal, they are unequal. Converse of neneqd 2424. One-way deduction form of df-ne 2404. (Contributed by David Moews, 28-Feb-2017.) Allow a shortening of necon3bi 2453. (Revised by Wolf Lammen, 22-Nov-2019.)

Hypothesis

Ref	Expression
neqned.1	|- ( ph -> -. A = B )

Assertion

Ref	Expression
neqned	|- ( ph -> A =/= B )

Proof of Theorem neqned

Step	Hyp	Ref	Expression
1		neqned.1	. 2 |- ( ph -> -. A = B )
2		df-ne 2404	. 2 |- ( A =/= B <-> -. A = B )
3	1, 2	sylibr 134	1 |- ( ph -> A =/= B )

Syntax hints:   -. wn 3   -> wi 4   = wceq 1398   =/= wne 2403

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This theorem depends on definitions:  df-bi 117  df-ne 2404

This theorem is referenced by:  neqne  2411  tfr1onlemsucaccv  6550  tfrcllemsucaccv  6563  enpr2d  7040  djune  7320  omp1eomlem  7336  difinfsn  7342  nnnninfeq2  7371  nninfisol  7375  netap  7516  2omotaplemap  7519  exmidapne  7522  xaddf  10123  xaddval  10124  xleaddadd  10166  flqltnz  10593  zfz1iso  11151  hashtpglem  11156  bezoutlemle  12642  eucalgval2  12688  eucalglt  12692  isprm2  12752  sqne2sq  12812  nnoddn2prmb  12898  ennnfonelemim  13108  ctinfomlemom  13111  hashfinmndnn  13578  logbgcd1irraplemexp  15762  lgsfcl2  15808  lgscllem  15809  lgsval2lem  15812  uhgr2edg  16130  eulerpathprum  16404  bj-charfunbi  16510  3dom  16691  pw1ndom3lem  16692  nnsf  16714  peano3nninf  16716  qdiff  16764  neapmkvlem  16783