Theorem neqned 2342

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

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1343   ≠ wne 2335

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 2336

This theorem is referenced by:  neqne  2343  tfr1onlemsucaccv  6305  tfrcllemsucaccv  6318  enpr2d  6779  djune  7039  omp1eomlem  7055  difinfsn  7061  nnnninfeq2  7089  nninfisol  7093  xaddf  9776  xaddval  9777  xleaddadd  9819  flqltnz  10218  zfz1iso  10750  bezoutlemle  11937  eucalgval2  11981  eucalglt  11985  lcmval  11991  lcmcllem  11995  isprm2  12045  sqne2sq  12105  nnoddn2prmb  12190  ennnfonelemim  12353  ctinfomlemom  12356  logbgcd1irraplemexp  13486  lgsfcl2  13507  lgscllem  13508  lgsval2lem  13511  bj-charfunbi  13653  nnsf  13845  peano3nninf  13847  neapmkvlem  13905