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  6612  tfrcllemsucaccv  6625  enpr2d  7111  djune  7418  omp1eomlem  7434  difinfsn  7440  nnnninfeq2  7469  nninfisol  7473  netap  7620  2omotaplemap  7623  exmidapne  7626  xaddf  10246  xaddval  10247  xleaddadd  10289  flqltnz  10722  zfz1iso  11293  hashtpglem  11298  bezoutlemle  12785  eucalgval2  12831  eucalglt  12835  isprm2  12895  sqne2sq  12955  nnoddn2prmb  13041  ballotfilemi1  13245  ballotfilemii  13246  ballotfilemfrcn0  13273  ennnfonelemim  13315  ctinfomlemom  13318  hashfinmndnn  13745  aprnzr  14599  logbgcd1irraplemexp  16070  lgsfcl2  16125  lgscllem  16126  lgsval2lem  16129  uhgr2edg  16447  eulerpathprum  16721  bj-charfunbi  16837  3dom  17018  pw1ndom3lem  17019  nnsf  17048  peano3nninf  17050  qdiff  17098  neapmkvlem  17117