Theorem neqned 2937

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

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

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 2931

This theorem is referenced by:  neqne  2938  necon3bi  2956  necon2ai  2959  necon3i  2962  mteqand  3021  nelne1  3027  nelne2  3028  ne0i  4292  rexn0  4462  nelpr2  4607  nelpr1  4608  otsndisj  5464  rnmptn0  6199  enpr2d  8980  sdomdif  9048  2pwne  9056  mapdom2  9071  dif1enlem  9079  infn0  9196  canthp1lem2  10554  nnneneg  12170  flltnz  13725  wrdlen2i  14859  s3sndisj  14884  isprm2  16603  isprm5  16628  nnoddn2prmb  16735  chnind  18537  chnccat  18542  hashfinmndnn  18669  sgrp2nmndlem5  18847  fincygsubgodd  20036  prmgrpsimpgd  20038  ornglmullt  20794  orngrmullt  20795  psdmul  22091  alexsub  23970  ioorf  25511  dvmptdiv  25915  dvtaylp  26315  cos02pilt1  26472  logccne0  26524  isosctrlem1  26765  isosctrlem2  26766  chordthmlem  26779  efrlim  26916  efrlimOLD  26917  lgsfcl2  27251  lgscllem  27252  lgsval2lem  27255  2sqn0  27382  2sqmod  27384  dchrisumn0  27469  noseponlem  27613  nosupbnd1lem3  27659  nosupbnd1lem4  27660  nosupbnd1lem5  27661  nosupbnd2lem1  27664  noinfbnd1lem3  27674  noinfbnd1lem4  27675  noinfbnd1lem5  27676  noetainflem4  27689  scutbdaybnd2lim  27768  tgbtwnne  28478  tgbtwndiff  28494  tgbtwnconn1lem3  28562  legov3  28586  legso  28587  ncolne1  28613  tglineneq  28632  tglowdim2ln  28639  mirne  28655  miriso  28658  mirhl  28667  mirbtwnhl  28668  symquadlem  28677  krippenlem  28678  midexlem  28680  ragflat3  28694  ragperp  28705  footexALT  28706  footexlem2  28708  colperpexlem2  28719  colperpexlem3  28720  mideulem2  28722  oppne3  28731  outpasch  28743  hlpasch  28744  lmieu  28772  lmicom  28776  axlowdim1  28948  wlkp1lem5  29665  wlkp1lem6  29666  eulerpathpr  30231  nmcfnlbi  32043  strlem1  32241  unidifsnne  32527  fsuppcurry1  32718  fsuppcurry2  32719  hashpss  32802  divnumden2  32809  xrge0npcan  33012  tocyccntz  33124  elrgspnlem4  33223  fracfld  33285  pidlnz  33352  drngidl  33409  drngidlhash  33410  rhmpreimaprmidl  33427  qsidomlem1  33428  qsnzr  33431  mxidlirredi  33447  mxidlirred  33448  ssmxidl  33450  krull  33455  krullndrng  33457  qsdrng  33473  rprmasso2  33502  rprmirred  33507  pidufd  33519  1arithufdlem3  33522  exsslsb  33620  constrextdg2lem  33772  constrext2chnlem  33774  2sqr3nconstr  33805  cos9thpinconstrlem2  33814  zarclsint  33896  zarclssn  33897  xrge0iifhom  33961  qqhf  34010  qqhre  34044  esumrnmpt2  34092  carsgclctunlem2  34343  ballotlemi1  34527  ballotlemii  34528  ballotlemfrcn0  34554  plymulx0  34571  signswn0  34584  signswch  34585  itgexpif  34630  repr0  34635  tgoldbachgtda  34685  pconnconn  35286  unbdqndv2lem2  36565  knoppndvlem13  36579  sucneqond  37420  finxpreclem2  37445  finxp1o  37447  maxidln0  38095  hdmapip0  42024  fldhmf1  42193  hashscontpow1  42224  aks6d1c6lem4  42276  aks6d1c7lem1  42283  remul01  42515  3cubeslem4  42796  3cubes  42797  pellexlem6  42941  nlimsuc  43548  scotteld  44353  mnuprdlem2  44380  inaex  44404  n0p  45156  disjrnmpt2  45299  dstregt0  45397  upbdrech2  45423  xrlexaddrp  45465  infleinflem2  45483  xrralrecnnge  45502  supminfxr2  45581  absimnre  45588  xrpnf  45597  ressioosup  45669  ressiooinf  45671  fmul01lt1lem1  45698  limcperiod  45742  climxrrelem  45861  sinaover2ne0  45980  fperdvper  46031  dvdivbd  46035  itgioocnicc  46089  stirlinglem5  46190  dirker2re  46204  dirkerdenne0  46205  dirkerper  46208  dirkertrigeqlem3  46212  dirkertrigeq  46213  dirkercncflem1  46215  dirkercncflem2  46216  dirkercncflem4  46218  fourierdlem24  46243  fourierdlem25  46244  fourierdlem40  46259  fourierdlem41  46260  fourierdlem42  46261  fourierdlem44  46263  fourierdlem48  46266  fourierdlem49  46267  fourierdlem57  46275  fourierdlem58  46276  fourierdlem59  46277  fourierdlem66  46284  fourierdlem68  46286  fourierdlem74  46292  fourierdlem75  46293  fourierdlem78  46296  fourierdlem80  46298  fourierdlem81  46299  fourierdlem109  46327  elaa2lem  46345  etransclem9  46355  etransclem35  46381  etransclem38  46384  sge0tsms  46492  sge0cl  46493  sge0fodjrnlem  46528  meadjun  46574  meadjiunlem  46577  hoicvr  46660  hoidmvlelem2  46708  hoiqssbllem3  46736  sigardiv  46973  sigarcol  46976  sharhght  46977  chnsubseq  46992  difltmodne  47456  minusmodnep2tmod  47467  modm1p1ne  47484  prmdvdsfmtnof1lem2  47699  gpg3kgrtriexlem5  48201  fucofvalne  49440  fullthinc  49565  euendfunc2  49642