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  6617  tfrcllemsucaccv  6630  enpr2d  7117  djune  7424  omp1eomlem  7440  difinfsn  7446  nnnninfeq2  7475  nninfisol  7479  netap  7626  2omotaplemap  7629  exmidapne  7632  xaddf  10262  xaddval  10263  xleaddadd  10305  flqltnz  10742  zfz1iso  11314  hashtpglem  11319  bezoutlemle  12809  eucalgval2  12855  eucalglt  12859  isprm2  12919  sqne2sq  12981  sqrtrirr  13013  nnoddn2prmb  13069  ballotfilemi1  13302  ballotfilemii  13303  ballotfilemfrcn0  13330  ennnfonelemim  13372  ctinfomlemom  13375  hashfinmndnn  13803  aprnzr  14707  logbgcd1irraplemexp  16221  lgsfcl2  16347  lgscllem  16348  lgsval2lem  16351  uhgr2edg  16669  eulerpathprum  16943  bj-charfunbi  17059  3dom  17240  pw1ndom3lem  17241  nnsf  17271  peano3nninf  17273  qdiff  17322  neapmkvlem  17341