Theorem neqned 2371

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

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

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 2365

This theorem is referenced by:  neqne  2372  tfr1onlemsucaccv  6396  tfrcllemsucaccv  6409  enpr2d  6873  djune  7139  omp1eomlem  7155  difinfsn  7161  nnnninfeq2  7190  nninfisol  7194  netap  7316  2omotaplemap  7319  exmidapne  7322  xaddf  9913  xaddval  9914  xleaddadd  9956  flqltnz  10359  zfz1iso  10915  bezoutlemle  12148  eucalgval2  12194  eucalglt  12198  isprm2  12258  sqne2sq  12318  nnoddn2prmb  12403  ennnfonelemim  12584  ctinfomlemom  12587  hashfinmndnn  13016  logbgcd1irraplemexp  15141  lgsfcl2  15163  lgscllem  15164  lgsval2lem  15167  bj-charfunbi  15373  nnsf  15565  peano3nninf  15567  neapmkvlem  15627