Theorem neqned 2316

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

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1332   ≠ wne 2309

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 2310

This theorem is referenced by:  neqne  2317  tfr1onlemsucaccv  6246  tfrcllemsucaccv  6259  enpr2d  6719  djune  6971  omp1eomlem  6987  difinfsn  6993  xaddf  9657  xaddval  9658  xleaddadd  9700  flqltnz  10091  zfz1iso  10616  bezoutlemle  11732  eucalgval2  11770  eucalglt  11774  lcmval  11780  lcmcllem  11784  isprm2  11834  sqne2sq  11891  ennnfonelemim  11973  ctinfomlemom  11976  logbgcd1irraplemexp  13093  nnsf  13374  peano3nninf  13376  neapmkvlem  13424