Theorem neqned 2933

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

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

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 2927

This theorem is referenced by:  neqne  2934  necon3bi  2952  necon2ai  2955  necon3i  2958  mteqand  3017  nelne1  3023  nelne2  3024  ne0i  4307  rexn0  4477  nelpr2  4620  nelpr1  4621  otsndisj  5482  rnmptn0  6220  enpr2d  9023  enpr2dOLD  9024  sdomdif  9095  2pwne  9103  mapdom2  9118  dif1enlem  9126  dif1enlemOLD  9127  infn0  9258  canthp1lem2  10613  nnneneg  12228  flltnz  13780  wrdlen2i  14915  s3sndisj  14940  isprm2  16659  isprm5  16684  nnoddn2prmb  16791  hashfinmndnn  18685  sgrp2nmndlem5  18863  fincygsubgodd  20051  prmgrpsimpgd  20053  psdmul  22060  alexsub  23939  ioorf  25481  dvmptdiv  25885  dvtaylp  26285  cos02pilt1  26442  logccne0  26494  isosctrlem1  26735  isosctrlem2  26736  chordthmlem  26749  efrlim  26886  efrlimOLD  26887  lgsfcl2  27221  lgscllem  27222  lgsval2lem  27225  2sqn0  27352  2sqmod  27354  dchrisumn0  27439  noseponlem  27583  nosupbnd1lem3  27629  nosupbnd1lem4  27630  nosupbnd1lem5  27631  nosupbnd2lem1  27634  noinfbnd1lem3  27644  noinfbnd1lem4  27645  noinfbnd1lem5  27646  noetainflem4  27659  scutbdaybnd2lim  27736  tgbtwnne  28424  tgbtwndiff  28440  tgbtwnconn1lem3  28508  legov3  28532  legso  28533  ncolne1  28559  tglineneq  28578  tglowdim2ln  28585  mirne  28601  miriso  28604  mirhl  28613  mirbtwnhl  28614  symquadlem  28623  krippenlem  28624  midexlem  28626  ragflat3  28640  ragperp  28651  footexALT  28652  footexlem2  28654  colperpexlem2  28665  colperpexlem3  28666  mideulem2  28668  oppne3  28677  outpasch  28689  hlpasch  28690  lmieu  28718  lmicom  28722  axlowdim1  28893  wlkp1lem5  29612  wlkp1lem6  29613  eulerpathpr  30176  nmcfnlbi  31988  strlem1  32186  unidifsnne  32472  fsuppcurry1  32655  fsuppcurry2  32656  hashpss  32741  divnumden2  32747  chnind  32944  xrge0npcan  32968  tocyccntz  33108  elrgspnlem4  33203  fracfld  33265  ornglmullt  33292  orngrmullt  33293  pidlnz  33354  drngidl  33411  drngidlhash  33412  rhmpreimaprmidl  33429  qsidomlem1  33430  qsnzr  33433  mxidlirredi  33449  mxidlirred  33450  ssmxidl  33452  krull  33457  krullndrng  33459  qsdrng  33475  rprmasso2  33504  rprmirred  33509  pidufd  33521  1arithufdlem3  33524  exsslsb  33599  constrextdg2lem  33745  constrext2chnlem  33747  2sqr3nconstr  33778  cos9thpinconstrlem2  33787  zarclsint  33869  zarclssn  33870  xrge0iifhom  33934  qqhf  33983  qqhre  34017  esumrnmpt2  34065  carsgclctunlem2  34317  ballotlemi1  34501  ballotlemii  34502  ballotlemfrcn0  34528  plymulx0  34545  signswn0  34558  signswch  34559  itgexpif  34604  repr0  34609  tgoldbachgtda  34659  pconnconn  35225  unbdqndv2lem2  36505  knoppndvlem13  36519  sucneqond  37360  finxpreclem2  37385  finxp1o  37387  maxidln0  38046  hdmapip0  41916  fldhmf1  42085  hashscontpow1  42116  aks6d1c6lem4  42168  aks6d1c7lem1  42175  remul01  42402  3cubeslem4  42684  3cubes  42685  pellexlem6  42829  nlimsuc  43437  scotteld  44242  mnuprdlem2  44269  inaex  44293  n0p  45046  disjrnmpt2  45189  dstregt0  45287  upbdrech2  45313  xrlexaddrp  45355  infleinflem2  45374  xrralrecnnge  45393  supminfxr2  45472  absimnre  45479  xrpnf  45488  ressioosup  45560  ressiooinf  45562  fmul01lt1lem1  45589  limcperiod  45633  climxrrelem  45754  sinaover2ne0  45873  fperdvper  45924  dvdivbd  45928  itgioocnicc  45982  stirlinglem5  46083  dirker2re  46097  dirkerdenne0  46098  dirkerper  46101  dirkertrigeqlem3  46105  dirkertrigeq  46106  dirkercncflem1  46108  dirkercncflem2  46109  dirkercncflem4  46111  fourierdlem24  46136  fourierdlem25  46137  fourierdlem40  46152  fourierdlem41  46153  fourierdlem42  46154  fourierdlem44  46156  fourierdlem48  46159  fourierdlem49  46160  fourierdlem57  46168  fourierdlem58  46169  fourierdlem59  46170  fourierdlem66  46177  fourierdlem68  46179  fourierdlem74  46185  fourierdlem75  46186  fourierdlem78  46189  fourierdlem80  46191  fourierdlem81  46192  fourierdlem109  46220  elaa2lem  46238  etransclem9  46248  etransclem35  46274  etransclem38  46277  sge0tsms  46385  sge0cl  46386  sge0fodjrnlem  46421  meadjun  46467  meadjiunlem  46470  hoicvr  46553  hoidmvlelem2  46601  hoiqssbllem3  46629  sigardiv  46866  sigarcol  46869  sharhght  46870  difltmodne  47347  minusmodnep2tmod  47358  modm1p1ne  47375  prmdvdsfmtnof1lem2  47590  gpg3kgrtriexlem5  48082  fucofvalne  49318  fullthinc  49443  euendfunc2  49520