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  6507  tfrcllemsucaccv  6520  enpr2d  6997  djune  7277  omp1eomlem  7293  difinfsn  7299  nnnninfeq2  7328  nninfisol  7332  netap  7473  2omotaplemap  7476  exmidapne  7479  xaddf  10079  xaddval  10080  xleaddadd  10122  flqltnz  10548  zfz1iso  11106  hashtpglem  11111  bezoutlemle  12597  eucalgval2  12643  eucalglt  12647  isprm2  12707  sqne2sq  12767  nnoddn2prmb  12853  ennnfonelemim  13063  ctinfomlemom  13066  hashfinmndnn  13533  logbgcd1irraplemexp  15711  lgsfcl2  15754  lgscllem  15755  lgsval2lem  15758  uhgr2edg  16076  eulerpathprum  16350  bj-charfunbi  16457  3dom  16638  pw1ndom3lem  16639  nnsf  16658  peano3nninf  16660  qdiff  16704  neapmkvlem  16723