Theorem neqned 2427

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

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   = wceq 1402   ≠ wne 2420

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This proof depends on definitions:  df-bi 117  df-ne 2421

This theorem is used by:  neqne  2428  tfr1onlemsucaccv  6612  tfrcllemsucaccv  6625  enpr2d  7111  djune  7419  omp1eomlem  7435  difinfsn  7441  nnnninfeq2  7470  nninfisol  7474  netap  7621  2omotaplemap  7624  exmidapne  7627  xaddf  10257  xaddval  10258  xleaddadd  10300  flqltnz  10737  zfz1iso  11309  hashtpglem  11314  bezoutlemle  12804  eucalgval2  12850  eucalglt  12854  isprm2  12914  sqne2sq  12976  sqrtrirr  13008  nnoddn2prmb  13064  ballotfilemi1  13297  ballotfilemii  13298  ballotfilemfrcn0  13325  ennnfonelemim  13367  ctinfomlemom  13370  hashfinmndnn  13798  aprnzr  14683  logbgcd1irraplemexp  16170  lgsfcl2  16296  lgscllem  16297  lgsval2lem  16300  uhgr2edg  16618  eulerpathprum  16892  bj-charfunbi  17008  3dom  17189  pw1ndom3lem  17190  nnsf  17219  peano3nninf  17221  qdiff  17270  neapmkvlem  17289