Theorem neqned 2354

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

Syntax hints:   -. wn 3   -> wi 4   = wceq 1353   =/= wne 2347

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 2348

This theorem is referenced by:  neqne  2355  tfr1onlemsucaccv  6344  tfrcllemsucaccv  6357  enpr2d  6819  djune  7079  omp1eomlem  7095  difinfsn  7101  nnnninfeq2  7129  nninfisol  7133  netap  7255  2omotaplemap  7258  exmidapne  7261  xaddf  9846  xaddval  9847  xleaddadd  9889  flqltnz  10289  zfz1iso  10823  bezoutlemle  12011  eucalgval2  12055  eucalglt  12059  lcmval  12065  lcmcllem  12069  isprm2  12119  sqne2sq  12179  nnoddn2prmb  12264  ennnfonelemim  12427  ctinfomlemom  12430  hashfinmndnn  12838  logbgcd1irraplemexp  14471  lgsfcl2  14492  lgscllem  14493  lgsval2lem  14496  bj-charfunbi  14648  nnsf  14839  peano3nninf  14841  neapmkvlem  14900