Theorem neqned 2374

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

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1364   ≠ wne 2367

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 2368

This theorem is referenced by:  neqne  2375  tfr1onlemsucaccv  6408  tfrcllemsucaccv  6421  enpr2d  6885  djune  7153  omp1eomlem  7169  difinfsn  7175  nnnninfeq2  7204  nninfisol  7208  netap  7339  2omotaplemap  7342  exmidapne  7345  xaddf  9938  xaddval  9939  xleaddadd  9981  flqltnz  10396  zfz1iso  10952  bezoutlemle  12202  eucalgval2  12248  eucalglt  12252  isprm2  12312  sqne2sq  12372  nnoddn2prmb  12458  ennnfonelemim  12668  ctinfomlemom  12671  hashfinmndnn  13136  logbgcd1irraplemexp  15290  lgsfcl2  15333  lgscllem  15334  lgsval2lem  15337  bj-charfunbi  15543  nnsf  15738  peano3nninf  15740  neapmkvlem  15802