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  4282  rexn0  4437  nelpr2  4598  nelpr1  4599  otsndisj  5474  rnmptn0  6209  enpr2d  8995  sdomdif  9063  2pwne  9071  mapdom2  9086  dif1enlem  9094  infn0  9212  canthp1lem2  10576  nnneneg  12212  flltnz  13770  wrdlen2i  14904  s3sndisj  14929  isprm2  16651  isprm5  16677  nnoddn2prmb  16784  chnind  18587  chnccat  18592  hashfinmndnn  18719  sgrp2nmndlem5  18900  fincygsubgodd  20089  prmgrpsimpgd  20091  ornglmullt  20846  orngrmullt  20847  psdmul  22132  alexsub  24010  ioorf  25540  dvmptdiv  25941  dvtaylp  26335  cos02pilt1  26490  logccne0  26542  isosctrlem1  26782  isosctrlem2  26783  chordthmlem  26796  efrlim  26933  lgsfcl2  27266  lgscllem  27267  lgsval2lem  27270  2sqn0  27397  2sqmod  27399  dchrisumn0  27484  noseponlem  27628  nosupbnd1lem3  27674  nosupbnd1lem4  27675  nosupbnd1lem5  27676  nosupbnd2lem1  27679  noinfbnd1lem3  27689  noinfbnd1lem4  27690  noinfbnd1lem5  27691  noetainflem4  27704  cutbdaybnd2lim  27789  bdayfinbndlem1  28459  z12bdaylem1  28462  tgbtwnne  28558  tgbtwndiff  28574  tgbtwnconn1lem3  28642  legov3  28666  legso  28667  ncolne1  28693  tglineneq  28712  tglowdim2ln  28719  mirne  28735  miriso  28738  mirhl  28747  mirbtwnhl  28748  symquadlem  28757  krippenlem  28758  midexlem  28760  ragflat3  28774  ragperp  28785  footexALT  28786  footexlem2  28788  colperpexlem2  28799  colperpexlem3  28800  mideulem2  28802  oppne3  28811  outpasch  28823  hlpasch  28824  lmieu  28852  lmicom  28856  axlowdim1  29028  wlkp1lem5  29744  wlkp1lem6  29745  eulerpathpr  30310  nmcfnlbi  32123  strlem1  32321  unidifsnne  32606  fsuppcurry1  32797  fsuppcurry2  32798  hashpss  32882  divnumden2  32889  xrge0npcan  33080  tocyccntz  33205  elrgspnlem4  33306  fracfld  33369  pidlnz  33436  drngidl  33493  drngidlhash  33494  rhmpreimaprmidl  33511  qsidomlem1  33512  qsnzr  33515  mxidlirredi  33531  mxidlirred  33532  ssmxidl  33534  krull  33539  krullndrng  33541  qsdrng  33557  rprmasso2  33586  rprmirred  33591  pidufd  33603  1arithufdlem3  33606  mplmulmvr  33683  esplyind  33719  vietadeg1  33722  exsslsb  33741  constrextdg2lem  33892  constrext2chnlem  33894  2sqr3nconstr  33925  cos9thpinconstrlem2  33934  zarclsint  34016  zarclssn  34017  xrge0iifhom  34081  qqhf  34130  qqhre  34164  esumrnmpt2  34212  carsgclctunlem2  34463  ballotlemi1  34647  ballotlemii  34648  ballotlemfrcn0  34674  plymulx0  34691  signswn0  34704  signswch  34705  itgexpif  34750  repr0  34755  tgoldbachgtda  34805  noinfepfnregs  35276  pconnconn  35413  unbdqndv2lem2  36770  knoppndvlem13  36784  qdiff  37641  sucneqond  37681  finxpreclem2  37706  finxp1o  37708  maxidln0  38366  hdmapip0  42361  fldhmf1  42529  hashscontpow1  42560  aks6d1c6lem4  42612  aks6d1c7lem1  42619  remul01  42839  3cubeslem4  43121  3cubes  43122  pellexlem6  43262  nlimsuc  43868  scotteld  44673  mnuprdlem2  44700  inaex  44724  n0p  45476  disjrnmpt2  45618  dstregt0  45715  upbdrech2  45741  xrlexaddrp  45782  infleinflem2  45800  xrralrecnnge  45819  supminfxr2  45897  absimnre  45904  xrpnf  45913  ressioosup  45985  ressiooinf  45987  fmul01lt1lem1  46014  limcperiod  46058  climxrrelem  46177  sinaover2ne0  46296  fperdvper  46347  dvdivbd  46351  itgioocnicc  46405  stirlinglem5  46506  dirker2re  46520  dirkerdenne0  46521  dirkerper  46524  dirkertrigeqlem3  46528  dirkertrigeq  46529  dirkercncflem1  46531  dirkercncflem2  46532  dirkercncflem4  46534  fourierdlem24  46559  fourierdlem25  46560  fourierdlem40  46575  fourierdlem41  46576  fourierdlem42  46577  fourierdlem44  46579  fourierdlem48  46582  fourierdlem49  46583  fourierdlem57  46591  fourierdlem58  46592  fourierdlem59  46593  fourierdlem66  46600  fourierdlem68  46602  fourierdlem74  46608  fourierdlem75  46609  fourierdlem78  46612  fourierdlem80  46614  fourierdlem81  46615  fourierdlem109  46643  elaa2lem  46661  etransclem9  46671  etransclem35  46697  etransclem38  46700  sge0tsms  46808  sge0cl  46809  sge0fodjrnlem  46844  meadjun  46890  meadjiunlem  46893  hoicvr  46976  hoidmvlelem2  47024  hoiqssbllem3  47052  sigardiv  47289  sigarcol  47292  sharhght  47293  chnsubseq  47308  difltmodne  47790  minusmodnep2tmod  47801  modm1p1ne  47818  prmdvdsfmtnof1lem2  48042  gpg3kgrtriexlem5  48557  fucofvalne  49794  fullthinc  49919  euendfunc2  49996