Theorem neqned 2354

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

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1353   ≠ wne 2347

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 2348

This theorem is referenced by:  neqne  2355  tfr1onlemsucaccv  6341  tfrcllemsucaccv  6354  enpr2d  6816  djune  7076  omp1eomlem  7092  difinfsn  7098  nnnninfeq2  7126  nninfisol  7130  netap  7252  2omotaplemap  7255  exmidapne  7258  xaddf  9843  xaddval  9844  xleaddadd  9886  flqltnz  10286  zfz1iso  10820  bezoutlemle  12008  eucalgval2  12052  eucalglt  12056  lcmval  12062  lcmcllem  12066  isprm2  12116  sqne2sq  12176  nnoddn2prmb  12261  ennnfonelemim  12424  ctinfomlemom  12427  hashfinmndnn  12832  logbgcd1irraplemexp  14356  lgsfcl2  14377  lgscllem  14378  lgsval2lem  14381  bj-charfunbi  14533  nnsf  14724  peano3nninf  14726  neapmkvlem  14784