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  10736  zfz1iso  11308  hashtpglem  11313  bezoutlemle  12803  eucalgval2  12849  eucalglt  12853  isprm2  12913  sqne2sq  12975  sqrtrirr  13007  nnoddn2prmb  13063  ballotfilemi1  13296  ballotfilemii  13297  ballotfilemfrcn0  13324  ennnfonelemim  13366  ctinfomlemom  13369  hashfinmndnn  13796  aprnzr  14650  logbgcd1irraplemexp  16126  lgsfcl2  16247  lgscllem  16248  lgsval2lem  16251  uhgr2edg  16569  eulerpathprum  16843  bj-charfunbi  16959  3dom  17140  pw1ndom3lem  17141  nnsf  17170  peano3nninf  17172  qdiff  17220  neapmkvlem  17239