Theorem neqned 2427

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

Syntax hints:   -. wn 3   -> wi 4   = wceq 1402   =/= wne 2420

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 2421

This theorem is referenced by:  neqne  2428  tfr1onlemsucaccv  6602  tfrcllemsucaccv  6615  enpr2d  7101  djune  7408  omp1eomlem  7424  difinfsn  7430  nnnninfeq2  7459  nninfisol  7463  netap  7610  2omotaplemap  7613  exmidapne  7616  xaddf  10225  xaddval  10226  xleaddadd  10268  flqltnz  10700  zfz1iso  11271  hashtpglem  11276  bezoutlemle  12763  eucalgval2  12809  eucalglt  12813  isprm2  12873  sqne2sq  12933  nnoddn2prmb  13019  ballotfilemi1  13223  ballotfilemii  13224  ballotfilemfrcn0  13251  ennnfonelemim  13293  ctinfomlemom  13296  hashfinmndnn  13722  aprnzr  14572  logbgcd1irraplemexp  15993  lgsfcl2  16039  lgscllem  16040  lgsval2lem  16043  uhgr2edg  16361  eulerpathprum  16635  bj-charfunbi  16751  3dom  16932  pw1ndom3lem  16933  nnsf  16953  peano3nninf  16955  qdiff  17003  neapmkvlem  17022