Theorem neqned 2940

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

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1542   ≠ wne 2933

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 2934

This theorem is referenced by:  neqne  2941  necon3bi  2959  necon2ai  2962  necon3i  2965  mteqand  3024  nelne1  3030  nelne2  3031  ne0i  4294  rexn0  4450  nelpr2  4611  nelpr1  4612  otsndisj  5468  rnmptn0  6203  enpr2d  8990  sdomdif  9058  2pwne  9066  mapdom2  9081  dif1enlem  9089  infn0  9207  canthp1lem2  10569  nnneneg  12185  flltnz  13736  wrdlen2i  14870  s3sndisj  14895  isprm2  16614  isprm5  16639  nnoddn2prmb  16746  chnind  18549  chnccat  18554  hashfinmndnn  18681  sgrp2nmndlem5  18859  fincygsubgodd  20048  prmgrpsimpgd  20050  ornglmullt  20807  orngrmullt  20808  psdmul  22114  alexsub  23994  ioorf  25535  dvmptdiv  25939  dvtaylp  26339  cos02pilt1  26496  logccne0  26548  isosctrlem1  26789  isosctrlem2  26790  chordthmlem  26803  efrlim  26940  efrlimOLD  26941  lgsfcl2  27275  lgscllem  27276  lgsval2lem  27279  2sqn0  27406  2sqmod  27408  dchrisumn0  27493  noseponlem  27637  nosupbnd1lem3  27683  nosupbnd1lem4  27684  nosupbnd1lem5  27685  nosupbnd2lem1  27688  noinfbnd1lem3  27698  noinfbnd1lem4  27699  noinfbnd1lem5  27700  noetainflem4  27713  cutbdaybnd2lim  27798  bdayfinbndlem1  28468  z12bdaylem1  28471  tgbtwnne  28567  tgbtwndiff  28583  tgbtwnconn1lem3  28651  legov3  28675  legso  28676  ncolne1  28702  tglineneq  28721  tglowdim2ln  28728  mirne  28744  miriso  28747  mirhl  28756  mirbtwnhl  28757  symquadlem  28766  krippenlem  28767  midexlem  28769  ragflat3  28783  ragperp  28794  footexALT  28795  footexlem2  28797  colperpexlem2  28808  colperpexlem3  28809  mideulem2  28811  oppne3  28820  outpasch  28832  hlpasch  28833  lmieu  28861  lmicom  28865  axlowdim1  29037  wlkp1lem5  29754  wlkp1lem6  29755  eulerpathpr  30320  nmcfnlbi  32132  strlem1  32330  unidifsnne  32615  fsuppcurry1  32806  fsuppcurry2  32807  hashpss  32892  divnumden2  32899  xrge0npcan  33105  tocyccntz  33230  elrgspnlem4  33331  fracfld  33394  pidlnz  33461  drngidl  33518  drngidlhash  33519  rhmpreimaprmidl  33536  qsidomlem1  33537  qsnzr  33540  mxidlirredi  33556  mxidlirred  33557  ssmxidl  33559  krull  33564  krullndrng  33566  qsdrng  33582  rprmasso2  33611  rprmirred  33616  pidufd  33628  1arithufdlem3  33631  mplmulmvr  33708  esplyind  33744  vietadeg1  33747  exsslsb  33766  constrextdg2lem  33918  constrext2chnlem  33920  2sqr3nconstr  33951  cos9thpinconstrlem2  33960  zarclsint  34042  zarclssn  34043  xrge0iifhom  34107  qqhf  34156  qqhre  34190  esumrnmpt2  34238  carsgclctunlem2  34489  ballotlemi1  34673  ballotlemii  34674  ballotlemfrcn0  34700  plymulx0  34717  signswn0  34730  signswch  34731  itgexpif  34776  repr0  34781  tgoldbachgtda  34831  noinfepfnregs  35301  pconnconn  35438  unbdqndv2lem2  36723  knoppndvlem13  36737  sucneqond  37583  finxpreclem2  37608  finxp1o  37610  maxidln0  38259  hdmapip0  42254  fldhmf1  42423  hashscontpow1  42454  aks6d1c6lem4  42506  aks6d1c7lem1  42513  remul01  42740  3cubeslem4  43009  3cubes  43010  pellexlem6  43154  nlimsuc  43760  scotteld  44565  mnuprdlem2  44592  inaex  44616  n0p  45368  disjrnmpt2  45510  dstregt0  45607  upbdrech2  45633  xrlexaddrp  45674  infleinflem2  45692  xrralrecnnge  45711  supminfxr2  45790  absimnre  45797  xrpnf  45806  ressioosup  45878  ressiooinf  45880  fmul01lt1lem1  45907  limcperiod  45951  climxrrelem  46070  sinaover2ne0  46189  fperdvper  46240  dvdivbd  46244  itgioocnicc  46298  stirlinglem5  46399  dirker2re  46413  dirkerdenne0  46414  dirkerper  46417  dirkertrigeqlem3  46421  dirkertrigeq  46422  dirkercncflem1  46424  dirkercncflem2  46425  dirkercncflem4  46427  fourierdlem24  46452  fourierdlem25  46453  fourierdlem40  46468  fourierdlem41  46469  fourierdlem42  46470  fourierdlem44  46472  fourierdlem48  46475  fourierdlem49  46476  fourierdlem57  46484  fourierdlem58  46485  fourierdlem59  46486  fourierdlem66  46493  fourierdlem68  46495  fourierdlem74  46501  fourierdlem75  46502  fourierdlem78  46505  fourierdlem80  46507  fourierdlem81  46508  fourierdlem109  46536  elaa2lem  46554  etransclem9  46564  etransclem35  46590  etransclem38  46593  sge0tsms  46701  sge0cl  46702  sge0fodjrnlem  46737  meadjun  46783  meadjiunlem  46786  hoicvr  46869  hoidmvlelem2  46917  hoiqssbllem3  46945  sigardiv  47182  sigarcol  47185  sharhght  47186  chnsubseq  47201  difltmodne  47665  minusmodnep2tmod  47676  modm1p1ne  47693  prmdvdsfmtnof1lem2  47908  gpg3kgrtriexlem5  48410  fucofvalne  49647  fullthinc  49772  euendfunc2  49849