Theorem neqned 2976

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

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1601   ≠ wne 2969

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 199  df-ne 2970

This theorem is referenced by:  neqne  2977  necon3bi  2995  necon2ai  2998  necon3i  3001  nelne1  3066  nelne2  3068  ne0i  4149  otsndisj  5216  sdomdif  8396  2pwne  8404  mapdom2  8419  canthp1lem2  9810  xrge0neqmnfOLD  12590  flltnz  12931  wrdlen2i  14093  s3sndisj  14115  isprm2  15800  isprm5  15823  nnoddn2prmb  15922  sgrp2nmndlem5  17803  maducoeval2  20851  alexsub  22257  ioorf  23777  dvmptdiv  24174  dvtaylp  24561  logccne0  24762  isosctrlem1  24996  isosctrlem2  24997  chordthmlem  25010  efrlim  25148  lgsfcl2  25480  lgscllem  25481  lgsval2lem  25484  dchrisumn0  25662  tgbtwnne  25841  tgbtwndiff  25857  tgbtwnconn1lem3  25925  legov3  25949  legso  25950  ncolne1  25976  tglineneq  25995  tglowdim2ln  26002  mirne  26018  miriso  26021  mirhl  26030  mirbtwnhl  26031  symquadlem  26040  krippenlem  26041  midexlem  26043  ragflat3  26057  ragperp  26068  footex  26069  colperpexlem2  26079  colperpexlem3  26080  mideulem2  26082  oppne3  26091  outpasch  26103  hlpasch  26104  lmieu  26132  lmicom  26136  axlowdim1  26308  wlkp1lem5  27028  wlkp1lem6  27029  eulerpathpr  27644  nmcfnlbi  29483  strlem1  29681  divnumden2  30128  2sqn0  30208  2sqmod  30210  xrge0npcan  30256  ornglmullt  30369  orngrmullt  30370  xrge0iifhom  30581  qqhf  30628  qqhre  30662  esumrnmpt2  30728  carsgclctunlem2  30979  ballotlemi1  31163  ballotlemii  31164  ballotlemfrcn0  31190  plymulx0  31224  signswn0  31237  signswch  31238  signstfvneq0  31250  itgexpif  31286  repr0  31291  tgoldbachgtda  31341  pconnconn  31812  noseponlem  32406  nosupbnd1lem3  32445  nosupbnd1lem4  32446  nosupbnd1lem5  32447  nosupbnd2lem1  32450  unbdqndv2lem2  33083  knoppndvlem13  33097  sucneqond  33808  finxpreclem2  33822  finxp1o  33824  maxidln0  34468  hdmapip0  38069  prjspersym  38208  pellexlem6  38358  n0p  40141  nelpr2  40192  nelpr1  40193  disjrnmpt2  40298  rnmptn0  40334  dstregt0  40403  upbdrech2  40431  xrlexaddrp  40476  infleinflem2  40495  xrralrecnnge  40519  supminfxr2  40604  absimnre  40612  xrpnf  40621  ressioosup  40690  ressiooinf  40692  fmul01lt1lem1  40724  limcperiod  40768  climxrrelem  40889  sinaover2ne0  41007  fperdvper  41061  dvdivbd  41066  itgioocnicc  41120  stirlinglem5  41222  dirker2re  41236  dirkerdenne0  41237  dirkerper  41240  dirkertrigeqlem3  41244  dirkertrigeq  41245  dirkercncflem1  41247  dirkercncflem2  41248  dirkercncflem4  41250  fourierdlem24  41275  fourierdlem25  41276  fourierdlem40  41291  fourierdlem41  41292  fourierdlem42  41293  fourierdlem44  41295  fourierdlem48  41298  fourierdlem49  41299  fourierdlem57  41307  fourierdlem58  41308  fourierdlem59  41309  fourierdlem66  41316  fourierdlem68  41318  fourierdlem74  41324  fourierdlem75  41325  fourierdlem78  41328  fourierdlem80  41330  fourierdlem81  41331  fourierdlem109  41359  elaa2lem  41377  etransclem9  41387  etransclem35  41413  etransclem38  41416  sge0tsms  41521  sge0cl  41522  sge0fodjrnlem  41557  meadjun  41603  meadjiunlem  41606  hoicvr  41689  hoidmvlelem2  41737  hoiqssbllem3  41765  sigardiv  41977  sigarcol  41980  sharhght  41981  prmdvdsfmtnof1lem2  42518  difmodm1lt  43332