Theorem neqned 2427

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

This proof depends on syntax axioms:   -. wn 3   -> wi 4   = wceq 1402   =/= wne 2420

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This proof depends on definitions:  df-bi 117  df-ne 2421

This theorem is used by:  neqne  2428  tfr1onlemsucaccv  6612  tfrcllemsucaccv  6625  enpr2d  7111  djune  7418  omp1eomlem  7434  difinfsn  7440  nnnninfeq2  7469  nninfisol  7473  netap  7620  2omotaplemap  7623  exmidapne  7626  xaddf  10256  xaddval  10257  xleaddadd  10299  flqltnz  10735  zfz1iso  11307  hashtpglem  11312  bezoutlemle  12801  eucalgval2  12847  eucalglt  12851  isprm2  12911  sqne2sq  12973  sqrtrirr  13005  nnoddn2prmb  13061  ballotfilemi1  13294  ballotfilemii  13295  ballotfilemfrcn0  13322  ennnfonelemim  13364  ctinfomlemom  13367  hashfinmndnn  13794  aprnzr  14648  logbgcd1irraplemexp  16123  lgsfcl2  16223  lgscllem  16224  lgsval2lem  16227  uhgr2edg  16545  eulerpathprum  16819  bj-charfunbi  16935  3dom  17116  pw1ndom3lem  17117  nnsf  17146  peano3nninf  17148  qdiff  17196  neapmkvlem  17215