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  7573  2omotaplemap  7576  exmidapne  7579  xaddf  10183  xaddval  10184  xleaddadd  10226  flqltnz  10654  zfz1iso  11221  hashtpglem  11226  bezoutlemle  12712  eucalgval2  12758  eucalglt  12762  isprm2  12822  sqne2sq  12882  nnoddn2prmb  12968  ennnfonelemim  13196  ctinfomlemom  13199  hashfinmndnn  13666  aprnzr  14459  logbgcd1irraplemexp  15882  lgsfcl2  15928  lgscllem  15929  lgsval2lem  15932  uhgr2edg  16250  eulerpathprum  16524  bj-charfunbi  16630  3dom  16811  pw1ndom3lem  16812  nnsf  16832  peano3nninf  16834  qdiff  16882  neapmkvlem  16902