Theorem neqned 2965

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

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1561   ≠ wne 2958

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 209  df-ne 2959

This theorem is referenced by:  neqne  2966  necon3bi  2984  necon2ai  2987  necon3i  2990  mteqand  3049  nelne1  3055  nelne2  3056  ne0i  4294  rexn0  4451  nelpr2  4613  nelpr1  4614  otsndisj  5489  rnmptn0  6231  enpr2d  9029  sdomdif  9097  2pwne  9105  mapdom2  9120  dif1enlem  9128  infn0  9246  scotteld  9856  canthp1lem2  10622  nnneneg  12258  flltnz  13831  wrdlen2i  14965  s3sndisj  14990  isprm2  16726  isprm5  16752  nnoddn2prmb  16859  chnind  18663  chnccat  18668  hashfinmndnn  18795  sgrp2nmndlem5  18976  fincygsubgodd  20164  prmgrpsimpgd  20166  ornglmullt  20925  orngrmullt  20926  psdmul  22238  alexsub  24112  ioorf  25642  dvmptdiv  26043  plyn0mulidp  26352  dvtaylp  26440  cos02pilt1  26598  logccne0  26650  isosctrlem1  26890  isosctrlem2  26891  chordthmlem  26904  efrlim  27041  lgsfcl2  27374  lgscllem  27375  lgsval2lem  27378  2sqn0  27505  2sqmod  27507  dchrisumn0  27592  noseponlem  27735  nosupbnd1lem3  27781  nosupbnd1lem4  27782  nosupbnd1lem5  27783  nosupbnd2lem1  27786  noinfbnd1lem3  27796  noinfbnd1lem4  27797  noinfbnd1lem5  27798  noetainflem4  27811  cutbdaybnd2lim  27897  bdayfinbndlem1  28567  z12bdaylem1  28570  tgbtwnne  28666  tgbtwndiff  28682  tgbtwnconn1lem3  28750  legov3  28774  legso  28775  ncolne1  28801  tglineneq  28821  tglowdim2ln  28828  mirne  28847  miriso  28850  mirhl  28859  mirbtwnhl  28860  symquadlem  28869  krippenlem  28870  midexlem  28872  ragflat3  28886  ragperp  28897  footexALT  28898  footexlem2  28900  colperpexlem2  28911  colperpexlem3  28912  mideulem2  28914  oppne3  28923  outpasch  28935  hlpasch  28936  lmieu  28964  lmicom  28968  plngrotlem1  29001  axlowdim1  29167  wlkp1lem5  29883  wlkp1lem6  29884  eulerpathpr  30449  nmcfnlbi  32262  strlem1  32460  unidifsnne  32741  fsuppcurry1  32932  fsuppcurry2  32933  hashpss  33017  divnumden2  33024  xrge0npcan  33204  tocyccntz  33330  elrgspnlem4  33432  fracfld  33498  pidlnz  33565  drngidl  33622  drngidlhash  33623  rhmpreimaprmidl  33641  qsidomlem1  33642  qsnzr  33645  mxidlirredi  33662  mxidlirred  33663  ssmxidl  33665  krull  33670  krullndrng  33672  qsdrng  33688  dflringlem  33693  rprmasso2  33725  rprmirred  33730  pidufd  33742  1arithufdlem3  33745  mplmulmvr  33838  esplyind  33874  vietadeg1  33877  exsslsb  33896  constrextdg2lem  34047  constrext2chnlem  34049  2sqr3nconstr  34080  cos9thpinconstrlem2  34089  zarclsint  34171  zarclssn  34172  xrge0iifhom  34236  qqhf  34285  qqhre  34319  esumrnmpt2  34367  carsgclctunlem2  34618  ballotlemi1  34802  ballotlemii  34803  ballotlemfrcn0  34829  signswn0  34856  signswch  34857  itgexpif  34902  repr0  34907  tgoldbachgtda  34957  morleylemrneab  34967  noinfepfnregs  35432  pconnconn  35586  unbdqndv2lem2  36953  knoppndvlem13  36967  qdiff  37824  sucneqond  37864  finxpreclem2  37889  finxp1o  37891  maxidln0  38549  hdmapip0  42544  fldhmf1  42712  hashscontpow1  42743  aks6d1c6lem4  42795  aks6d1c7lem1  42802  remul01  43021  3cubeslem4  43275  3cubes  43276  pellexlem6  43416  nlimsuc  44022  mnuprdlem2  44840  inaex  44864  n0p  45616  disjrnmpt2  45757  dstregt0  45852  upbdrech2  45878  xrlexaddrp  45919  infleinflem2  45937  xrralrecnnge  45956  supminfxr2  46034  absimnre  46041  xrpnf  46050  ressioosup  46122  ressiooinf  46124  fmul01lt1lem1  46151  limcperiod  46195  climxrrelem  46314  sinaover2ne0  46433  fperdvper  46484  dvdivbd  46488  itgioocnicc  46542  stirlinglem5  46643  dirker2re  46657  dirkerdenne0  46658  dirkerper  46661  dirkertrigeqlem3  46665  dirkertrigeq  46666  dirkercncflem1  46668  dirkercncflem2  46669  dirkercncflem4  46671  fourierdlem24  46696  fourierdlem25  46697  fourierdlem40  46712  fourierdlem41  46713  fourierdlem42  46714  fourierdlem44  46716  fourierdlem48  46719  fourierdlem49  46720  fourierdlem57  46728  fourierdlem58  46729  fourierdlem59  46730  fourierdlem66  46737  fourierdlem68  46739  fourierdlem74  46745  fourierdlem75  46746  fourierdlem78  46749  fourierdlem80  46751  fourierdlem81  46752  fourierdlem109  46780  elaa2lem  46798  etransclem9  46808  etransclem35  46834  etransclem38  46837  sge0tsms  46945  sge0cl  46946  sge0fodjrnlem  46981  meadjun  47027  meadjiunlem  47030  hoicvr  47113  hoidmvlelem2  47161  hoiqssbllem3  47189  sigardiv  47426  sigarcol  47429  sharhght  47430  chnsubseq  47447  difltmodne  47933  minusmodnep2tmod  47944  modm1p1ne  47961  prmdvdsfmtnof1lem2  48185  gpg3kgrtriexlem5  48700  fucofvalne  49937  fullthinc  50062  euendfunc2  50139