Theorem neqned 2944

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

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1536   ≠ wne 2937

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 207  df-ne 2938

This theorem is referenced by:  neqne  2945  necon3bi  2964  necon2ai  2967  necon3i  2970  mteqand  3030  nelne1  3036  nelne2  3037  ne0i  4346  rexn0  4516  nelpr2  4657  nelpr1  4658  otsndisj  5528  rnmptn0  6265  enpr2d  9087  enpr2dOLD  9088  sdomdif  9163  2pwne  9171  mapdom2  9186  dif1enlem  9194  dif1enlemOLD  9195  infn0  9337  canthp1lem2  10690  nnneneg  12298  flltnz  13847  wrdlen2i  14977  s3sndisj  15002  isprm2  16715  isprm5  16740  nnoddn2prmb  16846  hashfinmndnn  18776  sgrp2nmndlem5  18954  fincygsubgodd  20146  prmgrpsimpgd  20148  psdmul  22187  alexsub  24068  ioorf  25621  dvmptdiv  26026  dvtaylp  26426  cos02pilt1  26582  logccne0  26634  isosctrlem1  26875  isosctrlem2  26876  chordthmlem  26889  efrlim  27026  efrlimOLD  27027  lgsfcl2  27361  lgscllem  27362  lgsval2lem  27365  2sqn0  27492  2sqmod  27494  dchrisumn0  27579  noseponlem  27723  nosupbnd1lem3  27769  nosupbnd1lem4  27770  nosupbnd1lem5  27771  nosupbnd2lem1  27774  noinfbnd1lem3  27784  noinfbnd1lem4  27785  noinfbnd1lem5  27786  noetainflem4  27799  scutbdaybnd2lim  27876  tgbtwnne  28512  tgbtwndiff  28528  tgbtwnconn1lem3  28596  legov3  28620  legso  28621  ncolne1  28647  tglineneq  28666  tglowdim2ln  28673  mirne  28689  miriso  28692  mirhl  28701  mirbtwnhl  28702  symquadlem  28711  krippenlem  28712  midexlem  28714  ragflat3  28728  ragperp  28739  footexALT  28740  footexlem2  28742  colperpexlem2  28753  colperpexlem3  28754  mideulem2  28756  oppne3  28765  outpasch  28777  hlpasch  28778  lmieu  28806  lmicom  28810  axlowdim1  28988  wlkp1lem5  29709  wlkp1lem6  29710  eulerpathpr  30268  nmcfnlbi  32080  strlem1  32278  unidifsnne  32561  fsuppcurry1  32742  fsuppcurry2  32743  divnumden2  32821  chnind  32984  xrge0npcan  33007  tocyccntz  33146  elrgspnlem4  33234  fracfld  33289  ornglmullt  33316  orngrmullt  33317  pidlnz  33383  drngidl  33440  drngidlhash  33441  rhmpreimaprmidl  33458  qsidomlem1  33459  qsnzr  33462  mxidlirredi  33478  mxidlirred  33479  ssmxidl  33481  krull  33486  krullndrng  33488  qsdrng  33504  rprmasso2  33533  rprmirred  33538  pidufd  33550  1arithufdlem3  33553  zarclsint  33832  zarclssn  33833  xrge0iifhom  33897  qqhf  33948  qqhre  33982  esumrnmpt2  34048  carsgclctunlem2  34300  ballotlemi1  34483  ballotlemii  34484  ballotlemfrcn0  34510  plymulx0  34540  signswn0  34553  signswch  34554  itgexpif  34599  repr0  34604  tgoldbachgtda  34654  pconnconn  35215  unbdqndv2lem2  36492  knoppndvlem13  36506  sucneqond  37347  finxpreclem2  37372  finxp1o  37374  maxidln0  38031  hdmapip0  41897  fldhmf1  42071  hashscontpow1  42102  aks6d1c6lem4  42154  aks6d1c7lem1  42161  metakunt28  42213  metakunt30  42215  remul01  42413  3cubeslem4  42676  3cubes  42677  pellexlem6  42821  nlimsuc  43430  scotteld  44241  mnuprdlem2  44268  inaex  44292  n0p  44982  disjrnmpt2  45130  dstregt0  45231  upbdrech2  45258  xrlexaddrp  45301  infleinflem2  45320  xrralrecnnge  45339  supminfxr2  45418  absimnre  45426  xrpnf  45435  ressioosup  45507  ressiooinf  45509  fmul01lt1lem1  45539  limcperiod  45583  climxrrelem  45704  sinaover2ne0  45823  fperdvper  45874  dvdivbd  45878  itgioocnicc  45932  stirlinglem5  46033  dirker2re  46047  dirkerdenne0  46048  dirkerper  46051  dirkertrigeqlem3  46055  dirkertrigeq  46056  dirkercncflem1  46058  dirkercncflem2  46059  dirkercncflem4  46061  fourierdlem24  46086  fourierdlem25  46087  fourierdlem40  46102  fourierdlem41  46103  fourierdlem42  46104  fourierdlem44  46106  fourierdlem48  46109  fourierdlem49  46110  fourierdlem57  46118  fourierdlem58  46119  fourierdlem59  46120  fourierdlem66  46127  fourierdlem68  46129  fourierdlem74  46135  fourierdlem75  46136  fourierdlem78  46139  fourierdlem80  46141  fourierdlem81  46142  fourierdlem109  46170  elaa2lem  46188  etransclem9  46198  etransclem35  46224  etransclem38  46227  sge0tsms  46335  sge0cl  46336  sge0fodjrnlem  46371  meadjun  46417  meadjiunlem  46420  hoicvr  46503  hoidmvlelem2  46551  hoiqssbllem3  46579  sigardiv  46816  sigarcol  46819  sharhght  46820  difltmodne  47281  minusmodnep2tmod  47292  prmdvdsfmtnof1lem2  47509  difmodm1lt  48371  fullthinc  48845