Theorem neqned 2946

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

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

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 2940

This theorem is referenced by:  neqne  2947  necon3bi  2966  necon2ai  2969  necon3i  2972  mteqand  3032  nelne1  3038  nelne2  3039  ne0i  4299  rexn0  4473  nelpr2  4618  nelpr1  4619  otsndisj  5481  rnmptn0  6201  enpr2d  9000  enpr2dOLD  9001  sdomdif  9076  2pwne  9084  mapdom2  9099  dif1enlem  9107  dif1enlemOLD  9108  infn0  9258  canthp1lem2  10598  nnneneg  12197  flltnz  13726  wrdlen2i  14843  s3sndisj  14864  isprm2  16569  isprm5  16594  nnoddn2prmb  16696  hashfinmndnn  18587  sgrp2nmndlem5  18753  fincygsubgodd  19905  prmgrpsimpgd  19907  alexsub  23433  ioorf  24974  dvmptdiv  25375  dvtaylp  25766  cos02pilt1  25919  logccne0  25971  isosctrlem1  26205  isosctrlem2  26206  chordthmlem  26219  efrlim  26356  lgsfcl2  26688  lgscllem  26689  lgsval2lem  26692  2sqn0  26819  2sqmod  26821  dchrisumn0  26906  noseponlem  27049  nosupbnd1lem3  27095  nosupbnd1lem4  27096  nosupbnd1lem5  27097  nosupbnd2lem1  27100  noinfbnd1lem3  27110  noinfbnd1lem4  27111  noinfbnd1lem5  27112  noetainflem4  27125  scutbdaybnd2lim  27199  tgbtwnne  27495  tgbtwndiff  27511  tgbtwnconn1lem3  27579  legov3  27603  legso  27604  ncolne1  27630  tglineneq  27649  tglowdim2ln  27656  mirne  27672  miriso  27675  mirhl  27684  mirbtwnhl  27685  symquadlem  27694  krippenlem  27695  midexlem  27697  ragflat3  27711  ragperp  27722  footexALT  27723  footexlem2  27725  colperpexlem2  27736  colperpexlem3  27737  mideulem2  27739  oppne3  27748  outpasch  27760  hlpasch  27761  lmieu  27789  lmicom  27793  axlowdim1  27971  wlkp1lem5  28688  wlkp1lem6  28689  eulerpathpr  29247  nmcfnlbi  31057  strlem1  31255  unidifsnne  31527  fsuppcurry1  31710  fsuppcurry2  31711  divnumden2  31784  xrge0npcan  31955  tocyccntz  32063  ornglmullt  32173  orngrmullt  32174  pidlnz  32236  rhmpreimaprmidl  32300  qsidomlem1  32301  ssmxidl  32315  krull  32316  zarclsint  32542  zarclssn  32543  xrge0iifhom  32607  qqhf  32656  qqhre  32690  esumrnmpt2  32756  carsgclctunlem2  33008  ballotlemi1  33191  ballotlemii  33192  ballotlemfrcn0  33218  plymulx0  33248  signswn0  33261  signswch  33262  itgexpif  33308  repr0  33313  tgoldbachgtda  33363  pconnconn  33912  unbdqndv2lem2  35049  knoppndvlem13  35063  sucneqond  35909  finxpreclem2  35934  finxp1o  35936  maxidln0  36577  hdmapip0  40451  fldhmf1  40620  metakunt28  40677  metakunt30  40679  remul01  40934  3cubeslem4  41070  3cubes  41071  pellexlem6  41215  nlimsuc  41835  scotteld  42648  mnuprdlem2  42675  inaex  42699  n0p  43373  disjrnmpt2  43529  dstregt0  43636  upbdrech2  43663  xrlexaddrp  43707  infleinflem2  43726  xrralrecnnge  43745  supminfxr2  43824  absimnre  43832  xrpnf  43841  ressioosup  43913  ressiooinf  43915  fmul01lt1lem1  43945  limcperiod  43989  climxrrelem  44110  sinaover2ne0  44229  fperdvper  44280  dvdivbd  44284  itgioocnicc  44338  stirlinglem5  44439  dirker2re  44453  dirkerdenne0  44454  dirkerper  44457  dirkertrigeqlem3  44461  dirkertrigeq  44462  dirkercncflem1  44464  dirkercncflem2  44465  dirkercncflem4  44467  fourierdlem24  44492  fourierdlem25  44493  fourierdlem40  44508  fourierdlem41  44509  fourierdlem42  44510  fourierdlem44  44512  fourierdlem48  44515  fourierdlem49  44516  fourierdlem57  44524  fourierdlem58  44525  fourierdlem59  44526  fourierdlem66  44533  fourierdlem68  44535  fourierdlem74  44541  fourierdlem75  44542  fourierdlem78  44545  fourierdlem80  44547  fourierdlem81  44548  fourierdlem109  44576  elaa2lem  44594  etransclem9  44604  etransclem35  44630  etransclem38  44633  sge0tsms  44741  sge0cl  44742  sge0fodjrnlem  44777  meadjun  44823  meadjiunlem  44826  hoicvr  44909  hoidmvlelem2  44957  hoiqssbllem3  44985  sigardiv  45222  sigarcol  45225  sharhght  45226  prmdvdsfmtnof1lem2  45897  difmodm1lt  46728  fullthinc  47186