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  6394  tfrcllemsucaccv  6407  enpr2d  6871  djune  7137  omp1eomlem  7153  difinfsn  7159  nnnninfeq2  7188  nninfisol  7192  netap  7314  2omotaplemap  7317  exmidapne  7320  xaddf  9910  xaddval  9911  xleaddadd  9953  flqltnz  10356  zfz1iso  10912  bezoutlemle  12145  eucalgval2  12191  eucalglt  12195  isprm2  12255  sqne2sq  12315  nnoddn2prmb  12400  ennnfonelemim  12581  ctinfomlemom  12584  hashfinmndnn  13013  logbgcd1irraplemexp  15100  lgsfcl2  15122  lgscllem  15123  lgsval2lem  15126  bj-charfunbi  15303  nnsf  15495  peano3nninf  15497  neapmkvlem  15557