Theorem neqned 2364

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

Syntax hints:   -. wn 3   -> wi 4   = wceq 1363   =/= wne 2357

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 2358

This theorem is referenced by:  neqne  2365  tfr1onlemsucaccv  6356  tfrcllemsucaccv  6369  enpr2d  6831  djune  7091  omp1eomlem  7107  difinfsn  7113  nnnninfeq2  7141  nninfisol  7145  netap  7267  2omotaplemap  7270  exmidapne  7273  xaddf  9858  xaddval  9859  xleaddadd  9901  flqltnz  10301  zfz1iso  10835  bezoutlemle  12023  eucalgval2  12067  eucalglt  12071  lcmval  12077  lcmcllem  12081  isprm2  12131  sqne2sq  12191  nnoddn2prmb  12276  ennnfonelemim  12439  ctinfomlemom  12442  hashfinmndnn  12855  logbgcd1irraplemexp  14682  lgsfcl2  14703  lgscllem  14704  lgsval2lem  14707  bj-charfunbi  14859  nnsf  15051  peano3nninf  15053  neapmkvlem  15112