Theorem neqned 2313

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

Syntax hints:   -. wn 3   -> wi 4   = wceq 1331   =/= wne 2306

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107

This theorem depends on definitions:  df-bi 116  df-ne 2307

This theorem is referenced by:  neqne  2314  tfr1onlemsucaccv  6231  tfrcllemsucaccv  6244  enpr2d  6704  djune  6956  omp1eomlem  6972  difinfsn  6978  xaddf  9620  xaddval  9621  xleaddadd  9663  flqltnz  10053  zfz1iso  10577  bezoutlemle  11685  eucalgval2  11723  eucalglt  11727  lcmval  11733  lcmcllem  11737  isprm2  11787  sqne2sq  11844  ennnfonelemim  11926  ctinfomlemom  11929  nnsf  13188  peano3nninf  13190