Theorem neqned 2932

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

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1540   ≠ wne 2925

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 2926

This theorem is referenced by:  neqne  2933  necon3bi  2951  necon2ai  2954  necon3i  2957  mteqand  3016  nelne1  3022  nelne2  3023  ne0i  4294  rexn0  4464  nelpr2  4607  nelpr1  4608  otsndisj  5466  rnmptn0  6197  enpr2d  8981  sdomdif  9049  2pwne  9057  mapdom2  9072  dif1enlem  9080  dif1enlemOLD  9081  infn0  9209  canthp1lem2  10566  nnneneg  12181  flltnz  13733  wrdlen2i  14867  s3sndisj  14892  isprm2  16611  isprm5  16636  nnoddn2prmb  16743  hashfinmndnn  18643  sgrp2nmndlem5  18821  fincygsubgodd  20011  prmgrpsimpgd  20013  ornglmullt  20772  orngrmullt  20773  psdmul  22069  alexsub  23948  ioorf  25490  dvmptdiv  25894  dvtaylp  26294  cos02pilt1  26451  logccne0  26503  isosctrlem1  26744  isosctrlem2  26745  chordthmlem  26758  efrlim  26895  efrlimOLD  26896  lgsfcl2  27230  lgscllem  27231  lgsval2lem  27234  2sqn0  27361  2sqmod  27363  dchrisumn0  27448  noseponlem  27592  nosupbnd1lem3  27638  nosupbnd1lem4  27639  nosupbnd1lem5  27640  nosupbnd2lem1  27643  noinfbnd1lem3  27653  noinfbnd1lem4  27654  noinfbnd1lem5  27655  noetainflem4  27668  scutbdaybnd2lim  27746  tgbtwnne  28453  tgbtwndiff  28469  tgbtwnconn1lem3  28537  legov3  28561  legso  28562  ncolne1  28588  tglineneq  28607  tglowdim2ln  28614  mirne  28630  miriso  28633  mirhl  28642  mirbtwnhl  28643  symquadlem  28652  krippenlem  28653  midexlem  28655  ragflat3  28669  ragperp  28680  footexALT  28681  footexlem2  28683  colperpexlem2  28694  colperpexlem3  28695  mideulem2  28697  oppne3  28706  outpasch  28718  hlpasch  28719  lmieu  28747  lmicom  28751  axlowdim1  28922  wlkp1lem5  29639  wlkp1lem6  29640  eulerpathpr  30202  nmcfnlbi  32014  strlem1  32212  unidifsnne  32498  fsuppcurry1  32681  fsuppcurry2  32682  hashpss  32767  divnumden2  32773  chnind  32966  xrge0npcan  32987  tocyccntz  33099  elrgspnlem4  33195  fracfld  33257  pidlnz  33323  drngidl  33380  drngidlhash  33381  rhmpreimaprmidl  33398  qsidomlem1  33399  qsnzr  33402  mxidlirredi  33418  mxidlirred  33419  ssmxidl  33421  krull  33426  krullndrng  33428  qsdrng  33444  rprmasso2  33473  rprmirred  33478  pidufd  33490  1arithufdlem3  33493  exsslsb  33568  constrextdg2lem  33714  constrext2chnlem  33716  2sqr3nconstr  33747  cos9thpinconstrlem2  33756  zarclsint  33838  zarclssn  33839  xrge0iifhom  33903  qqhf  33952  qqhre  33986  esumrnmpt2  34034  carsgclctunlem2  34286  ballotlemi1  34470  ballotlemii  34471  ballotlemfrcn0  34497  plymulx0  34514  signswn0  34527  signswch  34528  itgexpif  34573  repr0  34578  tgoldbachgtda  34628  pconnconn  35203  unbdqndv2lem2  36483  knoppndvlem13  36497  sucneqond  37338  finxpreclem2  37363  finxp1o  37365  maxidln0  38024  hdmapip0  41894  fldhmf1  42063  hashscontpow1  42094  aks6d1c6lem4  42146  aks6d1c7lem1  42153  remul01  42380  3cubeslem4  42662  3cubes  42663  pellexlem6  42807  nlimsuc  43414  scotteld  44219  mnuprdlem2  44246  inaex  44270  n0p  45023  disjrnmpt2  45166  dstregt0  45264  upbdrech2  45290  xrlexaddrp  45332  infleinflem2  45351  xrralrecnnge  45370  supminfxr2  45449  absimnre  45456  xrpnf  45465  ressioosup  45537  ressiooinf  45539  fmul01lt1lem1  45566  limcperiod  45610  climxrrelem  45731  sinaover2ne0  45850  fperdvper  45901  dvdivbd  45905  itgioocnicc  45959  stirlinglem5  46060  dirker2re  46074  dirkerdenne0  46075  dirkerper  46078  dirkertrigeqlem3  46082  dirkertrigeq  46083  dirkercncflem1  46085  dirkercncflem2  46086  dirkercncflem4  46088  fourierdlem24  46113  fourierdlem25  46114  fourierdlem40  46129  fourierdlem41  46130  fourierdlem42  46131  fourierdlem44  46133  fourierdlem48  46136  fourierdlem49  46137  fourierdlem57  46145  fourierdlem58  46146  fourierdlem59  46147  fourierdlem66  46154  fourierdlem68  46156  fourierdlem74  46162  fourierdlem75  46163  fourierdlem78  46166  fourierdlem80  46168  fourierdlem81  46169  fourierdlem109  46197  elaa2lem  46215  etransclem9  46225  etransclem35  46251  etransclem38  46254  sge0tsms  46362  sge0cl  46363  sge0fodjrnlem  46398  meadjun  46444  meadjiunlem  46447  hoicvr  46530  hoidmvlelem2  46578  hoiqssbllem3  46606  sigardiv  46843  sigarcol  46846  sharhght  46847  difltmodne  47327  minusmodnep2tmod  47338  modm1p1ne  47355  prmdvdsfmtnof1lem2  47570  gpg3kgrtriexlem5  48062  fucofvalne  49298  fullthinc  49423  euendfunc2  49500