Theorem neqned 2347

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

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1348   ≠ wne 2340

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 2341

This theorem is referenced by:  neqne  2348  tfr1onlemsucaccv  6317  tfrcllemsucaccv  6330  enpr2d  6791  djune  7051  omp1eomlem  7067  difinfsn  7073  nnnninfeq2  7101  nninfisol  7105  xaddf  9788  xaddval  9789  xleaddadd  9831  flqltnz  10230  zfz1iso  10763  bezoutlemle  11950  eucalgval2  11994  eucalglt  11998  lcmval  12004  lcmcllem  12008  isprm2  12058  sqne2sq  12118  nnoddn2prmb  12203  ennnfonelemim  12366  ctinfomlemom  12369  hashfinmndnn  12655  logbgcd1irraplemexp  13639  lgsfcl2  13660  lgscllem  13661  lgsval2lem  13664  bj-charfunbi  13806  nnsf  13998  peano3nninf  14000  neapmkvlem  14058