Theorem neqned 2419

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

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

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 2413

This theorem is referenced by:  neqne  2420  tfr1onlemsucaccv  6572  tfrcllemsucaccv  6585  enpr2d  7064  djune  7369  omp1eomlem  7385  difinfsn  7391  nnnninfeq2  7420  nninfisol  7424  netap  7568  2omotaplemap  7571  exmidapne  7574  xaddf  10177  xaddval  10178  xleaddadd  10220  flqltnz  10647  zfz1iso  11213  hashtpglem  11218  bezoutlemle  12704  eucalgval2  12750  eucalglt  12754  isprm2  12814  sqne2sq  12874  nnoddn2prmb  12960  ennnfonelemim  13175  ctinfomlemom  13178  hashfinmndnn  13645  aprnzr  14433  logbgcd1irraplemexp  15833  lgsfcl2  15879  lgscllem  15880  lgsval2lem  15883  uhgr2edg  16201  eulerpathprum  16475  bj-charfunbi  16581  3dom  16762  pw1ndom3lem  16763  nnsf  16783  peano3nninf  16785  qdiff  16833  neapmkvlem  16853