Theorem neqned 2951

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

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1539   ≠ wne 2944

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 206  df-ne 2945

This theorem is referenced by:  neqne  2952  necon3bi  2971  necon2ai  2974  necon3i  2977  nelne1  3042  nelne2  3043  mteqand  3049  ne0i  4269  rexn0  4442  nelpr2  4589  nelpr1  4590  otsndisj  5434  rnmptn0  6152  enpr2d  8847  sdomdif  8921  2pwne  8929  mapdom2  8944  dif1enlem  8952  canthp1lem2  10418  nnneneg  12017  flltnz  13540  wrdlen2i  14664  s3sndisj  14687  isprm2  16396  isprm5  16421  nnoddn2prmb  16523  hashfinmndnn  18411  sgrp2nmndlem5  18577  fincygsubgodd  19724  prmgrpsimpgd  19726  alexsub  23205  ioorf  24746  dvmptdiv  25147  dvtaylp  25538  cos02pilt1  25691  logccne0  25743  isosctrlem1  25977  isosctrlem2  25978  chordthmlem  25991  efrlim  26128  lgsfcl2  26460  lgscllem  26461  lgsval2lem  26464  2sqn0  26591  2sqmod  26593  dchrisumn0  26678  tgbtwnne  26860  tgbtwndiff  26876  tgbtwnconn1lem3  26944  legov3  26968  legso  26969  ncolne1  26995  tglineneq  27014  tglowdim2ln  27021  mirne  27037  miriso  27040  mirhl  27049  mirbtwnhl  27050  symquadlem  27059  krippenlem  27060  midexlem  27062  ragflat3  27076  ragperp  27087  footexALT  27088  footexlem2  27090  colperpexlem2  27101  colperpexlem3  27102  mideulem2  27104  oppne3  27113  outpasch  27125  hlpasch  27126  lmieu  27154  lmicom  27158  axlowdim1  27336  wlkp1lem5  28054  wlkp1lem6  28055  eulerpathpr  28613  nmcfnlbi  30423  strlem1  30621  unidifsnne  30893  fsuppcurry1  31069  fsuppcurry2  31070  divnumden2  31141  xrge0npcan  31312  tocyccntz  31420  ornglmullt  31515  orngrmullt  31516  pidlnz  31580  rhmpreimaprmidl  31636  qsidomlem1  31637  ssmxidl  31651  krull  31652  zarclsint  31831  zarclssn  31832  xrge0iifhom  31896  qqhf  31945  qqhre  31979  esumrnmpt2  32045  carsgclctunlem2  32295  ballotlemi1  32478  ballotlemii  32479  ballotlemfrcn0  32505  plymulx0  32535  signswn0  32548  signswch  32549  itgexpif  32595  repr0  32600  tgoldbachgtda  32650  pconnconn  33202  noseponlem  33876  nosupbnd1lem3  33922  nosupbnd1lem4  33923  nosupbnd1lem5  33924  nosupbnd2lem1  33927  noinfbnd1lem3  33937  noinfbnd1lem4  33938  noinfbnd1lem5  33939  noetainflem4  33952  scutbdaybnd2lim  34020  unbdqndv2lem2  34699  knoppndvlem13  34713  sucneqond  35545  finxpreclem2  35570  finxp1o  35572  maxidln0  36212  hdmapip0  39936  metakunt28  40159  metakunt30  40161  remul01  40397  3cubeslem4  40518  3cubes  40519  pellexlem6  40663  nlimsuc  41055  scotteld  41871  mnuprdlem2  41898  inaex  41922  n0p  42598  disjrnmpt2  42733  dstregt0  42827  upbdrech2  42854  xrlexaddrp  42898  infleinflem2  42917  xrralrecnnge  42937  supminfxr2  43016  absimnre  43024  xrpnf  43033  ressioosup  43100  ressiooinf  43102  fmul01lt1lem1  43132  limcperiod  43176  climxrrelem  43297  sinaover2ne0  43416  fperdvper  43467  dvdivbd  43471  itgioocnicc  43525  stirlinglem5  43626  dirker2re  43640  dirkerdenne0  43641  dirkerper  43644  dirkertrigeqlem3  43648  dirkertrigeq  43649  dirkercncflem1  43651  dirkercncflem2  43652  dirkercncflem4  43654  fourierdlem24  43679  fourierdlem25  43680  fourierdlem40  43695  fourierdlem41  43696  fourierdlem42  43697  fourierdlem44  43699  fourierdlem48  43702  fourierdlem49  43703  fourierdlem57  43711  fourierdlem58  43712  fourierdlem59  43713  fourierdlem66  43720  fourierdlem68  43722  fourierdlem74  43728  fourierdlem75  43729  fourierdlem78  43732  fourierdlem80  43734  fourierdlem81  43735  fourierdlem109  43763  elaa2lem  43781  etransclem9  43791  etransclem35  43817  etransclem38  43820  sge0tsms  43925  sge0cl  43926  sge0fodjrnlem  43961  meadjun  44007  meadjiunlem  44010  hoicvr  44093  hoidmvlelem2  44141  hoiqssbllem3  44169  sigardiv  44388  sigarcol  44391  sharhght  44392  prmdvdsfmtnof1lem2  45048  difmodm1lt  45879  fullthinc  46338