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  10196  xaddval  10197  xleaddadd  10239  flqltnz  10671  zfz1iso  11238  hashtpglem  11243  bezoutlemle  12729  eucalgval2  12775  eucalglt  12779  isprm2  12839  sqne2sq  12899  nnoddn2prmb  12985  ballotfilemi1  13189  ballotfilemii  13190  ballotfilemfrcn0  13217  ennnfonelemim  13259  ctinfomlemom  13262  hashfinmndnn  13693  aprnzr  14537  logbgcd1irraplemexp  15959  lgsfcl2  16005  lgscllem  16006  lgsval2lem  16009  uhgr2edg  16327  eulerpathprum  16601  bj-charfunbi  16707  3dom  16888  pw1ndom3lem  16889  nnsf  16909  peano3nninf  16911  qdiff  16959  neapmkvlem  16979