Theorem neqned 2421

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

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1398   ≠ wne 2414

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This theorem depends on definitions:  df-bi 117  df-ne 2415

This theorem is referenced by:  neqne  2422  tfr1onlemsucaccv  6585  tfrcllemsucaccv  6598  enpr2d  7077  djune  7382  omp1eomlem  7398  difinfsn  7404  nnnninfeq2  7433  nninfisol  7437  netap  7584  2omotaplemap  7587  exmidapne  7590  xaddf  10199  xaddval  10200  xleaddadd  10242  flqltnz  10674  zfz1iso  11241  hashtpglem  11246  bezoutlemle  12732  eucalgval2  12778  eucalglt  12782  isprm2  12842  sqne2sq  12902  nnoddn2prmb  12988  ballotfilemi1  13192  ballotfilemii  13193  ballotfilemfrcn0  13220  ennnfonelemim  13262  ctinfomlemom  13265  hashfinmndnn  13696  aprnzr  14540  logbgcd1irraplemexp  15962  lgsfcl2  16008  lgscllem  16009  lgsval2lem  16012  uhgr2edg  16330  eulerpathprum  16604  bj-charfunbi  16720  3dom  16901  pw1ndom3lem  16902  nnsf  16922  peano3nninf  16924  qdiff  16972  neapmkvlem  16992