Theorem neqned 2409

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

Syntax hints:   -. wn 3   -> wi 4   = wceq 1397   =/= wne 2402

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 2403

This theorem is referenced by:  neqne  2410  tfr1onlemsucaccv  6506  tfrcllemsucaccv  6519  enpr2d  6996  djune  7276  omp1eomlem  7292  difinfsn  7298  nnnninfeq2  7327  nninfisol  7331  netap  7472  2omotaplemap  7475  exmidapne  7478  xaddf  10078  xaddval  10079  xleaddadd  10121  flqltnz  10546  zfz1iso  11104  bezoutlemle  12578  eucalgval2  12624  eucalglt  12628  isprm2  12688  sqne2sq  12748  nnoddn2prmb  12834  ennnfonelemim  13044  ctinfomlemom  13047  hashfinmndnn  13514  logbgcd1irraplemexp  15691  lgsfcl2  15734  lgscllem  15735  lgsval2lem  15738  uhgr2edg  16056  bj-charfunbi  16406  3dom  16587  pw1ndom3lem  16588  nnsf  16607  peano3nninf  16609  neapmkvlem  16671