Theorem neqned 2387

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

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1375   ≠ wne 2380

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 2381

This theorem is referenced by:  neqne  2388  tfr1onlemsucaccv  6457  tfrcllemsucaccv  6470  enpr2d  6942  djune  7213  omp1eomlem  7229  difinfsn  7235  nnnninfeq2  7264  nninfisol  7268  netap  7408  2omotaplemap  7411  exmidapne  7414  xaddf  10008  xaddval  10009  xleaddadd  10051  flqltnz  10474  zfz1iso  11030  bezoutlemle  12495  eucalgval2  12541  eucalglt  12545  isprm2  12605  sqne2sq  12665  nnoddn2prmb  12751  ennnfonelemim  12961  ctinfomlemom  12964  hashfinmndnn  13431  logbgcd1irraplemexp  15607  lgsfcl2  15650  lgscllem  15651  lgsval2lem  15654  uhgr2edg  15969  bj-charfunbi  16084  nnsf  16282  peano3nninf  16284  neapmkvlem  16346