Theorem neqned 2947

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

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1540   ≠ wne 2940

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 2941

This theorem is referenced by:  neqne  2948  necon3bi  2967  necon2ai  2970  necon3i  2973  mteqand  3033  nelne1  3039  nelne2  3040  ne0i  4341  rexn0  4511  nelpr2  4653  nelpr1  4654  otsndisj  5524  rnmptn0  6264  enpr2d  9089  enpr2dOLD  9090  sdomdif  9165  2pwne  9173  mapdom2  9188  dif1enlem  9196  dif1enlemOLD  9197  infn0  9340  canthp1lem2  10693  nnneneg  12301  flltnz  13851  wrdlen2i  14981  s3sndisj  15006  isprm2  16719  isprm5  16744  nnoddn2prmb  16851  hashfinmndnn  18764  sgrp2nmndlem5  18942  fincygsubgodd  20132  prmgrpsimpgd  20134  psdmul  22170  alexsub  24053  ioorf  25608  dvmptdiv  26012  dvtaylp  26412  cos02pilt1  26568  logccne0  26620  isosctrlem1  26861  isosctrlem2  26862  chordthmlem  26875  efrlim  27012  efrlimOLD  27013  lgsfcl2  27347  lgscllem  27348  lgsval2lem  27351  2sqn0  27478  2sqmod  27480  dchrisumn0  27565  noseponlem  27709  nosupbnd1lem3  27755  nosupbnd1lem4  27756  nosupbnd1lem5  27757  nosupbnd2lem1  27760  noinfbnd1lem3  27770  noinfbnd1lem4  27771  noinfbnd1lem5  27772  noetainflem4  27785  scutbdaybnd2lim  27862  tgbtwnne  28498  tgbtwndiff  28514  tgbtwnconn1lem3  28582  legov3  28606  legso  28607  ncolne1  28633  tglineneq  28652  tglowdim2ln  28659  mirne  28675  miriso  28678  mirhl  28687  mirbtwnhl  28688  symquadlem  28697  krippenlem  28698  midexlem  28700  ragflat3  28714  ragperp  28725  footexALT  28726  footexlem2  28728  colperpexlem2  28739  colperpexlem3  28740  mideulem2  28742  oppne3  28751  outpasch  28763  hlpasch  28764  lmieu  28792  lmicom  28796  axlowdim1  28974  wlkp1lem5  29695  wlkp1lem6  29696  eulerpathpr  30259  nmcfnlbi  32071  strlem1  32269  unidifsnne  32554  fsuppcurry1  32736  fsuppcurry2  32737  hashpss  32813  divnumden2  32817  chnind  33001  xrge0npcan  33025  tocyccntz  33164  elrgspnlem4  33249  fracfld  33310  ornglmullt  33337  orngrmullt  33338  pidlnz  33404  drngidl  33461  drngidlhash  33462  rhmpreimaprmidl  33479  qsidomlem1  33480  qsnzr  33483  mxidlirredi  33499  mxidlirred  33500  ssmxidl  33502  krull  33507  krullndrng  33509  qsdrng  33525  rprmasso2  33554  rprmirred  33559  pidufd  33571  1arithufdlem3  33574  exsslsb  33647  constrextdg2lem  33789  zarclsint  33871  zarclssn  33872  xrge0iifhom  33936  qqhf  33987  qqhre  34021  esumrnmpt2  34069  carsgclctunlem2  34321  ballotlemi1  34505  ballotlemii  34506  ballotlemfrcn0  34532  plymulx0  34562  signswn0  34575  signswch  34576  itgexpif  34621  repr0  34626  tgoldbachgtda  34676  pconnconn  35236  unbdqndv2lem2  36511  knoppndvlem13  36525  sucneqond  37366  finxpreclem2  37391  finxp1o  37393  maxidln0  38052  hdmapip0  41917  fldhmf1  42091  hashscontpow1  42122  aks6d1c6lem4  42174  aks6d1c7lem1  42181  metakunt28  42233  metakunt30  42235  remul01  42437  3cubeslem4  42700  3cubes  42701  pellexlem6  42845  nlimsuc  43454  scotteld  44265  mnuprdlem2  44292  inaex  44316  n0p  45050  disjrnmpt2  45193  dstregt0  45293  upbdrech2  45320  xrlexaddrp  45363  infleinflem2  45382  xrralrecnnge  45401  supminfxr2  45480  absimnre  45487  xrpnf  45496  ressioosup  45568  ressiooinf  45570  fmul01lt1lem1  45599  limcperiod  45643  climxrrelem  45764  sinaover2ne0  45883  fperdvper  45934  dvdivbd  45938  itgioocnicc  45992  stirlinglem5  46093  dirker2re  46107  dirkerdenne0  46108  dirkerper  46111  dirkertrigeqlem3  46115  dirkertrigeq  46116  dirkercncflem1  46118  dirkercncflem2  46119  dirkercncflem4  46121  fourierdlem24  46146  fourierdlem25  46147  fourierdlem40  46162  fourierdlem41  46163  fourierdlem42  46164  fourierdlem44  46166  fourierdlem48  46169  fourierdlem49  46170  fourierdlem57  46178  fourierdlem58  46179  fourierdlem59  46180  fourierdlem66  46187  fourierdlem68  46189  fourierdlem74  46195  fourierdlem75  46196  fourierdlem78  46199  fourierdlem80  46201  fourierdlem81  46202  fourierdlem109  46230  elaa2lem  46248  etransclem9  46258  etransclem35  46284  etransclem38  46287  sge0tsms  46395  sge0cl  46396  sge0fodjrnlem  46431  meadjun  46477  meadjiunlem  46480  hoicvr  46563  hoidmvlelem2  46611  hoiqssbllem3  46639  sigardiv  46876  sigarcol  46879  sharhght  46880  difltmodne  47344  minusmodnep2tmod  47355  prmdvdsfmtnof1lem2  47572  gpg3kgrtriexlem5  48043  difmodm1lt  48443  fucofvalne  49020  fullthinc  49099