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  4304  rexn0  4474  nelpr2  4617  nelpr1  4618  otsndisj  5479  rnmptn0  6217  enpr2d  9020  enpr2dOLD  9021  sdomdif  9089  2pwne  9097  mapdom2  9112  dif1enlem  9120  dif1enlemOLD  9121  infn0  9251  canthp1lem2  10606  nnneneg  12221  flltnz  13773  wrdlen2i  14908  s3sndisj  14933  isprm2  16652  isprm5  16677  nnoddn2prmb  16784  hashfinmndnn  18678  sgrp2nmndlem5  18856  fincygsubgodd  20044  prmgrpsimpgd  20046  psdmul  22053  alexsub  23932  ioorf  25474  dvmptdiv  25878  dvtaylp  26278  cos02pilt1  26435  logccne0  26487  isosctrlem1  26728  isosctrlem2  26729  chordthmlem  26742  efrlim  26879  efrlimOLD  26880  lgsfcl2  27214  lgscllem  27215  lgsval2lem  27218  2sqn0  27345  2sqmod  27347  dchrisumn0  27432  noseponlem  27576  nosupbnd1lem3  27622  nosupbnd1lem4  27623  nosupbnd1lem5  27624  nosupbnd2lem1  27627  noinfbnd1lem3  27637  noinfbnd1lem4  27638  noinfbnd1lem5  27639  noetainflem4  27652  scutbdaybnd2lim  27729  tgbtwnne  28417  tgbtwndiff  28433  tgbtwnconn1lem3  28501  legov3  28525  legso  28526  ncolne1  28552  tglineneq  28571  tglowdim2ln  28578  mirne  28594  miriso  28597  mirhl  28606  mirbtwnhl  28607  symquadlem  28616  krippenlem  28617  midexlem  28619  ragflat3  28633  ragperp  28644  footexALT  28645  footexlem2  28647  colperpexlem2  28658  colperpexlem3  28659  mideulem2  28661  oppne3  28670  outpasch  28682  hlpasch  28683  lmieu  28711  lmicom  28715  axlowdim1  28886  wlkp1lem5  29605  wlkp1lem6  29606  eulerpathpr  30169  nmcfnlbi  31981  strlem1  32179  unidifsnne  32465  fsuppcurry1  32648  fsuppcurry2  32649  hashpss  32734  divnumden2  32740  chnind  32937  xrge0npcan  32961  tocyccntz  33101  elrgspnlem4  33196  fracfld  33258  ornglmullt  33285  orngrmullt  33286  pidlnz  33347  drngidl  33404  drngidlhash  33405  rhmpreimaprmidl  33422  qsidomlem1  33423  qsnzr  33426  mxidlirredi  33442  mxidlirred  33443  ssmxidl  33445  krull  33450  krullndrng  33452  qsdrng  33468  rprmasso2  33497  rprmirred  33502  pidufd  33514  1arithufdlem3  33517  exsslsb  33592  constrextdg2lem  33738  constrext2chnlem  33740  2sqr3nconstr  33771  cos9thpinconstrlem2  33780  zarclsint  33862  zarclssn  33863  xrge0iifhom  33927  qqhf  33976  qqhre  34010  esumrnmpt2  34058  carsgclctunlem2  34310  ballotlemi1  34494  ballotlemii  34495  ballotlemfrcn0  34521  plymulx0  34538  signswn0  34551  signswch  34552  itgexpif  34597  repr0  34602  tgoldbachgtda  34652  pconnconn  35218  unbdqndv2lem2  36498  knoppndvlem13  36512  sucneqond  37353  finxpreclem2  37378  finxp1o  37380  maxidln0  38039  hdmapip0  41909  fldhmf1  42078  hashscontpow1  42109  aks6d1c6lem4  42161  aks6d1c7lem1  42168  remul01  42395  3cubeslem4  42677  3cubes  42678  pellexlem6  42822  nlimsuc  43430  scotteld  44235  mnuprdlem2  44262  inaex  44286  n0p  45039  disjrnmpt2  45182  dstregt0  45280  upbdrech2  45306  xrlexaddrp  45348  infleinflem2  45367  xrralrecnnge  45386  supminfxr2  45465  absimnre  45472  xrpnf  45481  ressioosup  45553  ressiooinf  45555  fmul01lt1lem1  45582  limcperiod  45626  climxrrelem  45747  sinaover2ne0  45866  fperdvper  45917  dvdivbd  45921  itgioocnicc  45975  stirlinglem5  46076  dirker2re  46090  dirkerdenne0  46091  dirkerper  46094  dirkertrigeqlem3  46098  dirkertrigeq  46099  dirkercncflem1  46101  dirkercncflem2  46102  dirkercncflem4  46104  fourierdlem24  46129  fourierdlem25  46130  fourierdlem40  46145  fourierdlem41  46146  fourierdlem42  46147  fourierdlem44  46149  fourierdlem48  46152  fourierdlem49  46153  fourierdlem57  46161  fourierdlem58  46162  fourierdlem59  46163  fourierdlem66  46170  fourierdlem68  46172  fourierdlem74  46178  fourierdlem75  46179  fourierdlem78  46182  fourierdlem80  46184  fourierdlem81  46185  fourierdlem109  46213  elaa2lem  46231  etransclem9  46241  etransclem35  46267  etransclem38  46270  sge0tsms  46378  sge0cl  46379  sge0fodjrnlem  46414  meadjun  46460  meadjiunlem  46463  hoicvr  46546  hoidmvlelem2  46594  hoiqssbllem3  46622  sigardiv  46859  sigarcol  46862  sharhght  46863  difltmodne  47343  minusmodnep2tmod  47354  modm1p1ne  47371  prmdvdsfmtnof1lem2  47586  gpg3kgrtriexlem5  48078  fucofvalne  49314  fullthinc  49439  euendfunc2  49516