Theorem neqned 2374

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

Syntax hints:   -. wn 3   -> wi 4   = wceq 1364   =/= wne 2367

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 2368

This theorem is referenced by:  neqne  2375  tfr1onlemsucaccv  6408  tfrcllemsucaccv  6421  enpr2d  6885  djune  7153  omp1eomlem  7169  difinfsn  7175  nnnninfeq2  7204  nninfisol  7208  netap  7337  2omotaplemap  7340  exmidapne  7343  xaddf  9936  xaddval  9937  xleaddadd  9979  flqltnz  10394  zfz1iso  10950  bezoutlemle  12200  eucalgval2  12246  eucalglt  12250  isprm2  12310  sqne2sq  12370  nnoddn2prmb  12456  ennnfonelemim  12666  ctinfomlemom  12669  hashfinmndnn  13134  logbgcd1irraplemexp  15288  lgsfcl2  15331  lgscllem  15332  lgsval2lem  15335  bj-charfunbi  15541  nnsf  15736  peano3nninf  15738  neapmkvlem  15798