Theorem neqned 2409

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

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

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 2403

This theorem is referenced by:  neqne  2410  tfr1onlemsucaccv  6507  tfrcllemsucaccv  6520  enpr2d  6997  djune  7277  omp1eomlem  7293  difinfsn  7299  nnnninfeq2  7328  nninfisol  7332  netap  7473  2omotaplemap  7476  exmidapne  7479  xaddf  10079  xaddval  10080  xleaddadd  10122  flqltnz  10548  zfz1iso  11106  bezoutlemle  12581  eucalgval2  12627  eucalglt  12631  isprm2  12691  sqne2sq  12751  nnoddn2prmb  12837  ennnfonelemim  13047  ctinfomlemom  13050  hashfinmndnn  13517  logbgcd1irraplemexp  15695  lgsfcl2  15738  lgscllem  15739  lgsval2lem  15742  uhgr2edg  16060  bj-charfunbi  16427  3dom  16608  pw1ndom3lem  16609  nnsf  16628  peano3nninf  16630  neapmkvlem  16692