Theorem neqned 2964

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

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

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-ne 2958

This theorem is used by:  neqne  2965  necon3bi  2983  necon2ai  2986  necon3i  2989  mteqand  3048  nelne1  3054  nelne2  3055  ne0i  4290  rexn0  4455  nelpr2  4617  nelpr1  4618  otsndisj  5500  rnmptn0  6244  enpr2d  9058  sdomdif  9126  2pwne  9134  mapdom2  9149  dif1enlem  9157  infn0  9275  scotteld  9889  canthp1lem2  10665  nnneneg  12298  flltnz  13874  hashpss  14476  wrdlen2i  15015  s3sndisj  15042  isprm2  16776  isprm5  16802  nnoddn2prmb  16909  chnind  18713  chnccat  18718  hashfinmndnn  18856  sgrp2nmndlem5  19042  fincygsubgodd  20242  prmgrpsimpgd  20244  ornglmullt  21036  orngrmullt  21037  pidlnz  21438  drngidl  21449  rhmpreimaprmidl  21543  qsidomlem1  21544  qsnzr  21547  psdmul  22395  alexsub  24272  ioorf  25802  dvmptdiv  26203  plyn0mulidp  26512  dvtaylp  26603  cos02pilt1  26761  logccne0  26813  isosctrlem1  27053  isosctrlem2  27054  chordthmlem  27067  efrlim  27204  lgsfcl2  27537  lgscllem  27538  lgsval2lem  27541  2sqn0  27668  2sqmod  27670  dchrisumn0  27755  noseponlem  27898  nosupbnd1lem3  27944  nosupbnd1lem4  27945  nosupbnd1lem5  27946  nosupbnd2lem1  27949  noinfbnd1lem3  27959  noinfbnd1lem4  27960  noinfbnd1lem5  27961  noetainflem4  27974  cutbdaybnd2lim  28060  bdayfinbndlem1  28730  z12bdaylem1  28733  tgbtwnne  28830  tgbtwndiff  28846  tgbtwnconn1lem3  28914  legov3  28938  legso  28939  ncolne1  28970  tglineneq  28990  tglowdim2ln  28997  mirne  29016  miriso  29019  mirhl  29028  mirbtwnhl  29029  symquadlem  29038  krippenlem  29039  midexlem  29041  symquadprlnglem  29042  ragflat3  29058  ragperp  29069  footexALT  29070  footexlem2  29072  colperpexlem2  29084  colperpexlem3  29085  mideulem2  29087  oppne3  29096  outpasch  29110  hlpasch  29111  plngrotlem1  29142  lmieu  29166  lmicom  29170  tgaaddcpbllem1  29226  tgaaddcpbllem2  29227  angmndaddeu1  29252  angmndaddov2lem  29260  prlngmolem1  29295  prlngmo2  29299  prlngplngtr  29302  prlnginn0  29303  prlngmid2  29304  symquadprlng  29305  quadcgrprlng  29309  axlowdim1  29402  wlkp1lem5  30121  wlkp1lem6  30122  eulerpathpr  30706  nmcfnlbi  32519  strlem1  32717  unidifsnne  32997  fsuppcurry1  33182  fsuppcurry2  33183  divnumden2  33273  xrge0npcan  33447  tocyccntz  33571  elrgspnlem4  33672  fracfld  33736  drngidlhash  33848  mxidlirredi  33861  mxidlirred  33862  ssmxidl  33864  krull  33868  krullndrng  33870  qsdrng  33886  dflringlem  33891  rprmasso2  33923  rprmirred  33928  pidufd  33940  1arithufdlem3  33943  mplmulmvr  34036  esplyind  34072  vietadeg1  34075  exsslsb  34094  constrextdg2lem  34245  constrext2chnlem  34247  2sqr3nconstr  34278  cos9thpinconstrlem2  34287  zarclsint  34369  zarclssn  34370  xrge0iifhom  34434  qqhf  34483  qqhre  34517  esumrnmpt2  34565  carsgclctunlem2  34817  ballotlemi1  35001  ballotlemii  35002  ballotlemfrcn0  35028  signswn0  35055  signswch  35056  itgexpif  35101  repr0  35106  tgoldbachgtda  35156  morleylemrneab  35166  noinfepfnregs  35645  pconnconn  35797  unbdqndv2lem2  37194  knoppndvlem13  37208  qdiff  38066  sucneqond  38106  finxpreclem2  38131  finxp1o  38133  maxidln0  38782  hdmapip0  42775  fldhmf1  42943  hashscontpow1  42974  aks6d1c6lem4  43026  aks6d1c7lem1  43033  remul01  43269  3cubeslem4  43521  3cubes  43522  pellexlem6  43662  nlimsuc  44268  mnuprdlem2  45084  inaex  45108  n0p  45866  disjrnmpt2  46007  dstregt0  46102  upbdrech2  46128  xrlexaddrp  46169  infleinflem2  46187  xrralrecnnge  46206  supminfxr2  46284  absimnre  46291  xrpnf  46300  ressioosup  46372  ressiooinf  46374  fmul01lt1lem1  46401  limcperiod  46445  climxrrelem  46564  sinaover2ne0  46683  fperdvper  46734  dvdivbd  46738  itgioocnicc  46792  stirlinglem5  46893  dirker2re  46907  dirkerdenne0  46908  dirkerper  46911  dirkertrigeqlem3  46915  dirkertrigeq  46916  dirkercncflem1  46918  dirkercncflem2  46919  dirkercncflem4  46921  fourierdlem24  46946  fourierdlem25  46947  fourierdlem40  46962  fourierdlem41  46963  fourierdlem42  46964  fourierdlem44  46966  fourierdlem48  46969  fourierdlem49  46970  fourierdlem57  46978  fourierdlem58  46979  fourierdlem59  46980  fourierdlem66  46987  fourierdlem68  46989  fourierdlem74  46995  fourierdlem75  46996  fourierdlem78  46999  fourierdlem80  47001  fourierdlem81  47002  fourierdlem109  47030  elaa2lem  47048  etransclem9  47058  etransclem35  47084  etransclem38  47087  sge0tsms  47195  sge0cl  47196  sge0fodjrnlem  47231  meadjun  47277  meadjiunlem  47280  hoicvr  47363  hoidmvlelem2  47411  hoiqssbllem3  47439  sigardiv  47676  sigarcol  47679  sharhght  47680  difltmodne  48223  minusmodnep2tmod  48234  modm1p1ne  48251  prmdvdsfmtnof1lem2  48475  gpg3kgrtriexlem5  48990  fucofvalne  50238  fullthinc  50363  euendfunc2  50440