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  6400  tfrcllemsucaccv  6413  enpr2d  6877  djune  7145  omp1eomlem  7161  difinfsn  7167  nnnninfeq2  7196  nninfisol  7200  netap  7323  2omotaplemap  7326  exmidapne  7329  xaddf  9921  xaddval  9922  xleaddadd  9964  flqltnz  10379  zfz1iso  10935  bezoutlemle  12185  eucalgval2  12231  eucalglt  12235  isprm2  12295  sqne2sq  12355  nnoddn2prmb  12441  ennnfonelemim  12651  ctinfomlemom  12654  hashfinmndnn  13083  logbgcd1irraplemexp  15214  lgsfcl2  15257  lgscllem  15258  lgsval2lem  15261  bj-charfunbi  15467  nnsf  15659  peano3nninf  15661  neapmkvlem  15721