Theorem neqned 2953

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

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1537   ≠ wne 2946

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 2947

This theorem is referenced by:  neqne  2954  necon3bi  2973  necon2ai  2976  necon3i  2979  mteqand  3039  nelne1  3045  nelne2  3046  ne0i  4364  rexn0  4534  nelpr2  4675  nelpr1  4676  otsndisj  5538  rnmptn0  6275  enpr2d  9115  enpr2dOLD  9116  sdomdif  9191  2pwne  9199  mapdom2  9214  dif1enlem  9222  dif1enlemOLD  9223  infn0  9368  canthp1lem2  10722  nnneneg  12328  flltnz  13862  wrdlen2i  14991  s3sndisj  15016  isprm2  16729  isprm5  16754  nnoddn2prmb  16860  hashfinmndnn  18789  sgrp2nmndlem5  18964  fincygsubgodd  20156  prmgrpsimpgd  20158  psdmul  22193  alexsub  24074  ioorf  25627  dvmptdiv  26032  dvtaylp  26430  cos02pilt1  26586  logccne0  26638  isosctrlem1  26879  isosctrlem2  26880  chordthmlem  26893  efrlim  27030  efrlimOLD  27031  lgsfcl2  27365  lgscllem  27366  lgsval2lem  27369  2sqn0  27496  2sqmod  27498  dchrisumn0  27583  noseponlem  27727  nosupbnd1lem3  27773  nosupbnd1lem4  27774  nosupbnd1lem5  27775  nosupbnd2lem1  27778  noinfbnd1lem3  27788  noinfbnd1lem4  27789  noinfbnd1lem5  27790  noetainflem4  27803  scutbdaybnd2lim  27880  tgbtwnne  28516  tgbtwndiff  28532  tgbtwnconn1lem3  28600  legov3  28624  legso  28625  ncolne1  28651  tglineneq  28670  tglowdim2ln  28677  mirne  28693  miriso  28696  mirhl  28705  mirbtwnhl  28706  symquadlem  28715  krippenlem  28716  midexlem  28718  ragflat3  28732  ragperp  28743  footexALT  28744  footexlem2  28746  colperpexlem2  28757  colperpexlem3  28758  mideulem2  28760  oppne3  28769  outpasch  28781  hlpasch  28782  lmieu  28810  lmicom  28814  axlowdim1  28992  wlkp1lem5  29713  wlkp1lem6  29714  eulerpathpr  30272  nmcfnlbi  32084  strlem1  32282  unidifsnne  32564  fsuppcurry1  32739  fsuppcurry2  32740  divnumden2  32819  chnind  32983  xrge0npcan  33006  tocyccntz  33137  fracfld  33275  ornglmullt  33302  orngrmullt  33303  pidlnz  33369  drngidl  33426  drngidlhash  33427  rhmpreimaprmidl  33444  qsidomlem1  33445  qsnzr  33448  mxidlirredi  33464  mxidlirred  33465  ssmxidl  33467  krull  33472  krullndrng  33474  qsdrng  33490  rprmasso2  33519  rprmirred  33524  pidufd  33536  1arithufdlem3  33539  zarclsint  33818  zarclssn  33819  xrge0iifhom  33883  qqhf  33932  qqhre  33966  esumrnmpt2  34032  carsgclctunlem2  34284  ballotlemi1  34467  ballotlemii  34468  ballotlemfrcn0  34494  plymulx0  34524  signswn0  34537  signswch  34538  itgexpif  34583  repr0  34588  tgoldbachgtda  34638  pconnconn  35199  unbdqndv2lem2  36476  knoppndvlem13  36490  sucneqond  37331  finxpreclem2  37356  finxp1o  37358  maxidln0  38005  hdmapip0  41872  fldhmf1  42047  hashscontpow1  42078  aks6d1c6lem4  42130  aks6d1c7lem1  42137  metakunt28  42189  metakunt30  42191  remul01  42383  3cubeslem4  42645  3cubes  42646  pellexlem6  42790  nlimsuc  43403  scotteld  44215  mnuprdlem2  44242  inaex  44266  n0p  44945  disjrnmpt2  45095  dstregt0  45196  upbdrech2  45223  xrlexaddrp  45267  infleinflem2  45286  xrralrecnnge  45305  supminfxr2  45384  absimnre  45392  xrpnf  45401  ressioosup  45473  ressiooinf  45475  fmul01lt1lem1  45505  limcperiod  45549  climxrrelem  45670  sinaover2ne0  45789  fperdvper  45840  dvdivbd  45844  itgioocnicc  45898  stirlinglem5  45999  dirker2re  46013  dirkerdenne0  46014  dirkerper  46017  dirkertrigeqlem3  46021  dirkertrigeq  46022  dirkercncflem1  46024  dirkercncflem2  46025  dirkercncflem4  46027  fourierdlem24  46052  fourierdlem25  46053  fourierdlem40  46068  fourierdlem41  46069  fourierdlem42  46070  fourierdlem44  46072  fourierdlem48  46075  fourierdlem49  46076  fourierdlem57  46084  fourierdlem58  46085  fourierdlem59  46086  fourierdlem66  46093  fourierdlem68  46095  fourierdlem74  46101  fourierdlem75  46102  fourierdlem78  46105  fourierdlem80  46107  fourierdlem81  46108  fourierdlem109  46136  elaa2lem  46154  etransclem9  46164  etransclem35  46190  etransclem38  46193  sge0tsms  46301  sge0cl  46302  sge0fodjrnlem  46337  meadjun  46383  meadjiunlem  46386  hoicvr  46469  hoidmvlelem2  46517  hoiqssbllem3  46545  sigardiv  46782  sigarcol  46785  sharhght  46786  prmdvdsfmtnof1lem2  47459  difmodm1lt  48256  fullthinc  48713