Theorem neqned 2407

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

Syntax hints:   -. wn 3   -> wi 4   = wceq 1395   =/= wne 2400

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 2401

This theorem is referenced by:  neqne  2408  tfr1onlemsucaccv  6485  tfrcllemsucaccv  6498  enpr2d  6970  djune  7241  omp1eomlem  7257  difinfsn  7263  nnnninfeq2  7292  nninfisol  7296  netap  7436  2omotaplemap  7439  exmidapne  7442  xaddf  10036  xaddval  10037  xleaddadd  10079  flqltnz  10502  zfz1iso  11058  bezoutlemle  12524  eucalgval2  12570  eucalglt  12574  isprm2  12634  sqne2sq  12694  nnoddn2prmb  12780  ennnfonelemim  12990  ctinfomlemom  12993  hashfinmndnn  13460  logbgcd1irraplemexp  15636  lgsfcl2  15679  lgscllem  15680  lgsval2lem  15683  uhgr2edg  15998  bj-charfunbi  16132  nnsf  16330  peano3nninf  16332  neapmkvlem  16394