Theorem neqned 2421

Description: If it is not the case that two classes are equal, they are unequal. Converse of neneqd 2435. One-way deduction form of df-ne 2415. (Contributed by David Moews, 28-Feb-2017.) Allow a shortening of necon3bi 2464. (Revised by Wolf Lammen, 22-Nov-2019.)

Hypothesis

Ref	Expression
neqned.1	⊢ (𝜑 → ¬ 𝐴 = 𝐵)

Assertion

Ref	Expression
neqned	⊢ (𝜑 → 𝐴 ≠ 𝐵)

Proof of Theorem neqned

Step	Hyp	Ref	Expression
1		neqned.1	. 2 ⊢ (𝜑 → ¬ 𝐴 = 𝐵)
2		df-ne 2415	. 2 ⊢ (𝐴 ≠ 𝐵 ↔ ¬ 𝐴 = 𝐵)
3	1, 2	sylibr 134	1 ⊢ (𝜑 → 𝐴 ≠ 𝐵)

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1398   ≠ wne 2414

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 2415

This theorem is referenced by:  neqne  2422  tfr1onlemsucaccv  6574  tfrcllemsucaccv  6587  enpr2d  7066  djune  7371  omp1eomlem  7387  difinfsn  7393  nnnninfeq2  7422  nninfisol  7426  netap  7570  2omotaplemap  7573  exmidapne  7576  xaddf  10180  xaddval  10181  xleaddadd  10223  flqltnz  10651  zfz1iso  11217  hashtpglem  11222  bezoutlemle  12708  eucalgval2  12754  eucalglt  12758  isprm2  12818  sqne2sq  12878  nnoddn2prmb  12964  ennnfonelemim  13192  ctinfomlemom  13195  hashfinmndnn  13662  aprnzr  14450  logbgcd1irraplemexp  15850  lgsfcl2  15896  lgscllem  15897  lgsval2lem  15900  uhgr2edg  16218  eulerpathprum  16492  bj-charfunbi  16598  3dom  16779  pw1ndom3lem  16780  nnsf  16800  peano3nninf  16802  qdiff  16850  neapmkvlem  16870