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  6399  tfrcllemsucaccv  6412  enpr2d  6876  djune  7144  omp1eomlem  7160  difinfsn  7166  nnnninfeq2  7195  nninfisol  7199  netap  7321  2omotaplemap  7324  exmidapne  7327  xaddf  9919  xaddval  9920  xleaddadd  9962  flqltnz  10377  zfz1iso  10933  bezoutlemle  12175  eucalgval2  12221  eucalglt  12225  isprm2  12285  sqne2sq  12345  nnoddn2prmb  12431  ennnfonelemim  12641  ctinfomlemom  12644  hashfinmndnn  13073  logbgcd1irraplemexp  15204  lgsfcl2  15247  lgscllem  15248  lgsval2lem  15251  bj-charfunbi  15457  nnsf  15649  peano3nninf  15651  neapmkvlem  15711