Theorem neqned 2933

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

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1541   ≠ wne 2926

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 2927

This theorem is referenced by:  neqne  2934  necon3bi  2952  necon2ai  2955  necon3i  2958  mteqand  3017  nelne1  3023  nelne2  3024  ne0i  4289  rexn0  4459  nelpr2  4604  nelpr1  4605  otsndisj  5457  rnmptn0  6188  enpr2d  8965  sdomdif  9033  2pwne  9041  mapdom2  9056  dif1enlem  9064  infn0  9181  canthp1lem2  10536  nnneneg  12152  flltnz  13707  wrdlen2i  14841  s3sndisj  14866  isprm2  16585  isprm5  16610  nnoddn2prmb  16717  chnind  18519  chnccat  18524  hashfinmndnn  18651  sgrp2nmndlem5  18829  fincygsubgodd  20019  prmgrpsimpgd  20021  ornglmullt  20777  orngrmullt  20778  psdmul  22074  alexsub  23953  ioorf  25494  dvmptdiv  25898  dvtaylp  26298  cos02pilt1  26455  logccne0  26507  isosctrlem1  26748  isosctrlem2  26749  chordthmlem  26762  efrlim  26899  efrlimOLD  26900  lgsfcl2  27234  lgscllem  27235  lgsval2lem  27238  2sqn0  27365  2sqmod  27367  dchrisumn0  27452  noseponlem  27596  nosupbnd1lem3  27642  nosupbnd1lem4  27643  nosupbnd1lem5  27644  nosupbnd2lem1  27647  noinfbnd1lem3  27657  noinfbnd1lem4  27658  noinfbnd1lem5  27659  noetainflem4  27672  scutbdaybnd2lim  27751  tgbtwnne  28461  tgbtwndiff  28477  tgbtwnconn1lem3  28545  legov3  28569  legso  28570  ncolne1  28596  tglineneq  28615  tglowdim2ln  28622  mirne  28638  miriso  28641  mirhl  28650  mirbtwnhl  28651  symquadlem  28660  krippenlem  28661  midexlem  28663  ragflat3  28677  ragperp  28688  footexALT  28689  footexlem2  28691  colperpexlem2  28702  colperpexlem3  28703  mideulem2  28705  oppne3  28714  outpasch  28726  hlpasch  28727  lmieu  28755  lmicom  28759  axlowdim1  28930  wlkp1lem5  29647  wlkp1lem6  29648  eulerpathpr  30210  nmcfnlbi  32022  strlem1  32220  unidifsnne  32506  fsuppcurry1  32697  fsuppcurry2  32698  hashpss  32781  divnumden2  32788  xrge0npcan  32991  tocyccntz  33103  elrgspnlem4  33202  fracfld  33264  pidlnz  33331  drngidl  33388  drngidlhash  33389  rhmpreimaprmidl  33406  qsidomlem1  33407  qsnzr  33410  mxidlirredi  33426  mxidlirred  33427  ssmxidl  33429  krull  33434  krullndrng  33436  qsdrng  33452  rprmasso2  33481  rprmirred  33486  pidufd  33498  1arithufdlem3  33501  exsslsb  33599  constrextdg2lem  33751  constrext2chnlem  33753  2sqr3nconstr  33784  cos9thpinconstrlem2  33793  zarclsint  33875  zarclssn  33876  xrge0iifhom  33940  qqhf  33989  qqhre  34023  esumrnmpt2  34071  carsgclctunlem2  34322  ballotlemi1  34506  ballotlemii  34507  ballotlemfrcn0  34533  plymulx0  34550  signswn0  34563  signswch  34564  itgexpif  34609  repr0  34614  tgoldbachgtda  34664  pconnconn  35243  unbdqndv2lem2  36523  knoppndvlem13  36537  sucneqond  37378  finxpreclem2  37403  finxp1o  37405  maxidln0  38064  hdmapip0  41933  fldhmf1  42102  hashscontpow1  42133  aks6d1c6lem4  42185  aks6d1c7lem1  42192  remul01  42419  3cubeslem4  42701  3cubes  42702  pellexlem6  42846  nlimsuc  43453  scotteld  44258  mnuprdlem2  44285  inaex  44309  n0p  45061  disjrnmpt2  45204  dstregt0  45302  upbdrech2  45328  xrlexaddrp  45370  infleinflem2  45388  xrralrecnnge  45407  supminfxr2  45486  absimnre  45493  xrpnf  45502  ressioosup  45574  ressiooinf  45576  fmul01lt1lem1  45603  limcperiod  45647  climxrrelem  45766  sinaover2ne0  45885  fperdvper  45936  dvdivbd  45940  itgioocnicc  45994  stirlinglem5  46095  dirker2re  46109  dirkerdenne0  46110  dirkerper  46113  dirkertrigeqlem3  46117  dirkertrigeq  46118  dirkercncflem1  46120  dirkercncflem2  46121  dirkercncflem4  46123  fourierdlem24  46148  fourierdlem25  46149  fourierdlem40  46164  fourierdlem41  46165  fourierdlem42  46166  fourierdlem44  46168  fourierdlem48  46171  fourierdlem49  46172  fourierdlem57  46180  fourierdlem58  46181  fourierdlem59  46182  fourierdlem66  46189  fourierdlem68  46191  fourierdlem74  46197  fourierdlem75  46198  fourierdlem78  46201  fourierdlem80  46203  fourierdlem81  46204  fourierdlem109  46232  elaa2lem  46250  etransclem9  46260  etransclem35  46286  etransclem38  46289  sge0tsms  46397  sge0cl  46398  sge0fodjrnlem  46433  meadjun  46479  meadjiunlem  46482  hoicvr  46565  hoidmvlelem2  46613  hoiqssbllem3  46641  sigardiv  46878  sigarcol  46881  sharhght  46882  difltmodne  47352  minusmodnep2tmod  47363  modm1p1ne  47380  prmdvdsfmtnof1lem2  47595  gpg3kgrtriexlem5  48097  fucofvalne  49336  fullthinc  49461  euendfunc2  49538