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 1542   ≠ 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  4271  rexn0  4426  nelpr2  4587  nelpr1  4588  otsndisj  5462  rnmptn0  6197  enpr2d  8984  sdomdif  9052  2pwne  9060  mapdom2  9075  dif1enlem  9083  infn0  9201  canthp1lem2  10565  nnneneg  12201  flltnz  13759  wrdlen2i  14893  s3sndisj  14918  isprm2  16640  isprm5  16666  nnoddn2prmb  16773  chnind  18576  chnccat  18581  hashfinmndnn  18708  sgrp2nmndlem5  18889  fincygsubgodd  20078  prmgrpsimpgd  20080  ornglmullt  20835  orngrmullt  20836  psdmul  22121  alexsub  23998  ioorf  25528  dvmptdiv  25929  dvtaylp  26323  cos02pilt1  26478  logccne0  26530  isosctrlem1  26770  isosctrlem2  26771  chordthmlem  26784  efrlim  26921  lgsfcl2  27254  lgscllem  27255  lgsval2lem  27258  2sqn0  27385  2sqmod  27387  dchrisumn0  27472  noseponlem  27616  nosupbnd1lem3  27662  nosupbnd1lem4  27663  nosupbnd1lem5  27664  nosupbnd2lem1  27667  noinfbnd1lem3  27677  noinfbnd1lem4  27678  noinfbnd1lem5  27679  noetainflem4  27692  cutbdaybnd2lim  27777  bdayfinbndlem1  28447  z12bdaylem1  28450  tgbtwnne  28546  tgbtwndiff  28562  tgbtwnconn1lem3  28630  legov3  28654  legso  28655  ncolne1  28681  tglineneq  28700  tglowdim2ln  28707  mirne  28723  miriso  28726  mirhl  28735  mirbtwnhl  28736  symquadlem  28745  krippenlem  28746  midexlem  28748  ragflat3  28762  ragperp  28773  footexALT  28774  footexlem2  28776  colperpexlem2  28787  colperpexlem3  28788  mideulem2  28790  oppne3  28799  outpasch  28811  hlpasch  28812  lmieu  28840  lmicom  28844  axlowdim1  29016  wlkp1lem5  29732  wlkp1lem6  29733  eulerpathpr  30298  nmcfnlbi  32111  strlem1  32309  unidifsnne  32594  fsuppcurry1  32785  fsuppcurry2  32786  hashpss  32870  divnumden2  32877  xrge0npcan  33068  tocyccntz  33193  elrgspnlem4  33294  fracfld  33357  pidlnz  33424  drngidl  33481  drngidlhash  33482  rhmpreimaprmidl  33499  qsidomlem1  33500  qsnzr  33503  mxidlirredi  33519  mxidlirred  33520  ssmxidl  33522  krull  33527  krullndrng  33529  qsdrng  33545  rprmasso2  33574  rprmirred  33579  pidufd  33591  1arithufdlem3  33594  mplmulmvr  33671  esplyind  33707  vietadeg1  33710  exsslsb  33729  constrextdg2lem  33880  constrext2chnlem  33882  2sqr3nconstr  33913  cos9thpinconstrlem2  33922  zarclsint  34004  zarclssn  34005  xrge0iifhom  34069  qqhf  34118  qqhre  34152  esumrnmpt2  34200  carsgclctunlem2  34451  ballotlemi1  34635  ballotlemii  34636  ballotlemfrcn0  34662  plymulx0  34679  signswn0  34692  signswch  34693  itgexpif  34738  repr0  34743  tgoldbachgtda  34793  noinfepfnregs  35264  pconnconn  35401  unbdqndv2lem2  36758  knoppndvlem13  36772  qdiff  37629  sucneqond  37669  finxpreclem2  37694  finxp1o  37696  maxidln0  38354  hdmapip0  42349  fldhmf1  42517  hashscontpow1  42548  aks6d1c6lem4  42600  aks6d1c7lem1  42607  remul01  42827  3cubeslem4  43109  3cubes  43110  pellexlem6  43250  nlimsuc  43856  scotteld  44661  mnuprdlem2  44688  inaex  44712  n0p  45464  disjrnmpt2  45606  dstregt0  45703  upbdrech2  45729  xrlexaddrp  45770  infleinflem2  45788  xrralrecnnge  45807  supminfxr2  45885  absimnre  45892  xrpnf  45901  ressioosup  45973  ressiooinf  45975  fmul01lt1lem1  46002  limcperiod  46046  climxrrelem  46165  sinaover2ne0  46284  fperdvper  46335  dvdivbd  46339  itgioocnicc  46393  stirlinglem5  46494  dirker2re  46508  dirkerdenne0  46509  dirkerper  46512  dirkertrigeqlem3  46516  dirkertrigeq  46517  dirkercncflem1  46519  dirkercncflem2  46520  dirkercncflem4  46522  fourierdlem24  46547  fourierdlem25  46548  fourierdlem40  46563  fourierdlem41  46564  fourierdlem42  46565  fourierdlem44  46567  fourierdlem48  46570  fourierdlem49  46571  fourierdlem57  46579  fourierdlem58  46580  fourierdlem59  46581  fourierdlem66  46588  fourierdlem68  46590  fourierdlem74  46596  fourierdlem75  46597  fourierdlem78  46600  fourierdlem80  46602  fourierdlem81  46603  fourierdlem109  46631  elaa2lem  46649  etransclem9  46659  etransclem35  46685  etransclem38  46688  sge0tsms  46796  sge0cl  46797  sge0fodjrnlem  46832  meadjun  46878  meadjiunlem  46881  hoicvr  46964  hoidmvlelem2  47012  hoiqssbllem3  47040  sigardiv  47277  sigarcol  47280  sharhght  47281  chnsubseq  47298  difltmodne  47784  minusmodnep2tmod  47795  modm1p1ne  47812  prmdvdsfmtnof1lem2  48036  gpg3kgrtriexlem5  48551  fucofvalne  49788  fullthinc  49913  euendfunc2  49990