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 )

This proof depends on syntax axioms:   -. wn 3   -> wi 4   = wceq 1402   =/= wne 2420

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This proof depends on definitions:  df-bi 117  df-ne 2421

This theorem is used by:  neqne  2428  tfr1onlemsucaccv  6616  tfrcllemsucaccv  6629  enpr2d  7115  djune  7424  omp1eomlem  7440  difinfsn  7446  nnnninfeq2  7475  nninfisol  7479  netap  7626  2omotaplemap  7629  exmidapne  7632  xaddf  10263  xaddval  10264  xleaddadd  10306  flqltnz  10743  zfz1iso  11315  hashtpglem  11320  bezoutlemle  12810  eucalgval2  12856  eucalglt  12860  isprm2  12920  sqne2sq  12982  sqrtrirr  13014  nnoddn2prmb  13070  ballotfilemi1  13303  ballotfilemii  13304  ballotfilemfrcn0  13331  ennnfonelemim  13373  ctinfomlemom  13376  hashfinmndnn  13804  aprnzr  14708  logbgcd1irraplemexp  16204  lgsfcl2  16330  lgscllem  16331  lgsval2lem  16334  uhgr2edg  16652  eulerpathprum  16926  bj-charfunbi  17042  3dom  17223  pw1ndom3lem  17224  nnsf  17254  peano3nninf  17256  qdiff  17305  neapmkvlem  17324