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  6502  tfrcllemsucaccv  6515  enpr2d  6992  djune  7268  omp1eomlem  7284  difinfsn  7290  nnnninfeq2  7319  nninfisol  7323  netap  7463  2omotaplemap  7466  exmidapne  7469  xaddf  10069  xaddval  10070  xleaddadd  10112  flqltnz  10537  zfz1iso  11095  bezoutlemle  12569  eucalgval2  12615  eucalglt  12619  isprm2  12679  sqne2sq  12739  nnoddn2prmb  12825  ennnfonelemim  13035  ctinfomlemom  13038  hashfinmndnn  13505  logbgcd1irraplemexp  15682  lgsfcl2  15725  lgscllem  15726  lgsval2lem  15729  uhgr2edg  16045  bj-charfunbi  16342  3dom  16523  pw1ndom3lem  16524  nnsf  16543  peano3nninf  16545  neapmkvlem  16607