Theorem neqned 2408

Description: If it is not the case that two classes are equal, they are unequal. Converse of neneqd 2422. One-way deduction form of df-ne 2402. (Contributed by David Moews, 28-Feb-2017.) Allow a shortening of necon3bi 2451. (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 2402	. 2 ⊢ (𝐴 ≠ 𝐵 ↔ ¬ 𝐴 = 𝐵)
3	1, 2	sylibr 134	1 ⊢ (𝜑 → 𝐴 ≠ 𝐵)

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1397   ≠ wne 2401

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 2402

This theorem is referenced by:  neqne  2409  tfr1onlemsucaccv  6512  tfrcllemsucaccv  6525  enpr2d  7002  djune  7282  omp1eomlem  7298  difinfsn  7304  nnnninfeq2  7333  nninfisol  7337  netap  7478  2omotaplemap  7481  exmidapne  7484  xaddf  10084  xaddval  10085  xleaddadd  10127  flqltnz  10553  zfz1iso  11111  hashtpglem  11116  bezoutlemle  12602  eucalgval2  12648  eucalglt  12652  isprm2  12712  sqne2sq  12772  nnoddn2prmb  12858  ennnfonelemim  13068  ctinfomlemom  13071  hashfinmndnn  13538  logbgcd1irraplemexp  15721  lgsfcl2  15764  lgscllem  15765  lgsval2lem  15768  uhgr2edg  16086  eulerpathprum  16360  bj-charfunbi  16466  3dom  16647  pw1ndom3lem  16648  nnsf  16670  peano3nninf  16672  qdiff  16720  neapmkvlem  16739