Theorem neqned 2407

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

Syntax hints:   -. wn 3   -> wi 4   = wceq 1395   =/= wne 2400

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 2401

This theorem is referenced by:  neqne  2408  tfr1onlemsucaccv  6493  tfrcllemsucaccv  6506  enpr2d  6980  djune  7256  omp1eomlem  7272  difinfsn  7278  nnnninfeq2  7307  nninfisol  7311  netap  7451  2omotaplemap  7454  exmidapne  7457  xaddf  10052  xaddval  10053  xleaddadd  10095  flqltnz  10519  zfz1iso  11076  bezoutlemle  12544  eucalgval2  12590  eucalglt  12594  isprm2  12654  sqne2sq  12714  nnoddn2prmb  12800  ennnfonelemim  13010  ctinfomlemom  13013  hashfinmndnn  13480  logbgcd1irraplemexp  15657  lgsfcl2  15700  lgscllem  15701  lgsval2lem  15704  uhgr2edg  16019  bj-charfunbi  16229  3dom  16411  pw1ndom3lem  16412  nnsf  16431  peano3nninf  16433  neapmkvlem  16495