Theorem neqned 2347

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

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1348   ≠ wne 2340

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107

This theorem depends on definitions:  df-bi 116  df-ne 2341

This theorem is referenced by:  neqne  2348  tfr1onlemsucaccv  6320  tfrcllemsucaccv  6333  enpr2d  6795  djune  7055  omp1eomlem  7071  difinfsn  7077  nnnninfeq2  7105  nninfisol  7109  xaddf  9801  xaddval  9802  xleaddadd  9844  flqltnz  10243  zfz1iso  10776  bezoutlemle  11963  eucalgval2  12007  eucalglt  12011  lcmval  12017  lcmcllem  12021  isprm2  12071  sqne2sq  12131  nnoddn2prmb  12216  ennnfonelemim  12379  ctinfomlemom  12382  hashfinmndnn  12668  logbgcd1irraplemexp  13680  lgsfcl2  13701  lgscllem  13702  lgsval2lem  13705  bj-charfunbi  13846  nnsf  14038  peano3nninf  14040  neapmkvlem  14098