Theorem neqned 2384

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

Syntax hints:   -. wn 3   -> wi 4   = wceq 1373   =/= wne 2377

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 2378

This theorem is referenced by:  neqne  2385  tfr1onlemsucaccv  6440  tfrcllemsucaccv  6453  enpr2d  6925  djune  7195  omp1eomlem  7211  difinfsn  7217  nnnninfeq2  7246  nninfisol  7250  netap  7386  2omotaplemap  7389  exmidapne  7392  xaddf  9986  xaddval  9987  xleaddadd  10029  flqltnz  10452  zfz1iso  11008  bezoutlemle  12404  eucalgval2  12450  eucalglt  12454  isprm2  12514  sqne2sq  12574  nnoddn2prmb  12660  ennnfonelemim  12870  ctinfomlemom  12873  hashfinmndnn  13339  logbgcd1irraplemexp  15515  lgsfcl2  15558  lgscllem  15559  lgsval2lem  15562  bj-charfunbi  15885  nnsf  16083  peano3nninf  16085  neapmkvlem  16147