Theorem neqned 2421

Description: If it is not the case that two classes are equal, they are unequal. Converse of neneqd 2435. One-way deduction form of df-ne 2415. (Contributed by David Moews, 28-Feb-2017.) Allow a shortening of necon3bi 2464. (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 2415	. 2 |- ( A =/= B <-> -. A = B )
3	1, 2	sylibr 134	1 |- ( ph -> A =/= B )

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

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 2415

This theorem is referenced by:  neqne  2422  tfr1onlemsucaccv  6585  tfrcllemsucaccv  6598  enpr2d  7077  djune  7382  omp1eomlem  7398  difinfsn  7404  nnnninfeq2  7433  nninfisol  7437  netap  7584  2omotaplemap  7587  exmidapne  7590  xaddf  10199  xaddval  10200  xleaddadd  10242  flqltnz  10674  zfz1iso  11241  hashtpglem  11246  bezoutlemle  12733  eucalgval2  12779  eucalglt  12783  isprm2  12843  sqne2sq  12903  nnoddn2prmb  12989  ballotfilemi1  13193  ballotfilemii  13194  ballotfilemfrcn0  13221  ennnfonelemim  13263  ctinfomlemom  13266  hashfinmndnn  13697  aprnzr  14541  logbgcd1irraplemexp  15963  lgsfcl2  16009  lgscllem  16010  lgsval2lem  16013  uhgr2edg  16331  eulerpathprum  16605  bj-charfunbi  16721  3dom  16902  pw1ndom3lem  16903  nnsf  16923  peano3nninf  16925  qdiff  16973  neapmkvlem  16992