Theorem neqned 2943

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

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1534   ≠ wne 2936

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 206  df-ne 2937

This theorem is referenced by:  neqne  2944  necon3bi  2963  necon2ai  2966  necon3i  2969  mteqand  3029  nelne1  3035  nelne2  3036  ne0i  4331  rexn0  4507  nelpr2  4652  nelpr1  4653  otsndisj  5516  rnmptn0  6243  enpr2d  9068  enpr2dOLD  9069  sdomdif  9144  2pwne  9152  mapdom2  9167  dif1enlem  9175  dif1enlemOLD  9176  infn0  9326  canthp1lem2  10671  nnneneg  12272  flltnz  13803  wrdlen2i  14920  s3sndisj  14941  isprm2  16647  isprm5  16672  nnoddn2prmb  16776  hashfinmndnn  18705  sgrp2nmndlem5  18875  fincygsubgodd  20063  prmgrpsimpgd  20065  psdmul  22084  alexsub  23943  ioorf  25496  dvmptdiv  25900  dvtaylp  26299  cos02pilt1  26454  logccne0  26506  isosctrlem1  26744  isosctrlem2  26745  chordthmlem  26758  efrlim  26895  efrlimOLD  26896  lgsfcl2  27230  lgscllem  27231  lgsval2lem  27234  2sqn0  27361  2sqmod  27363  dchrisumn0  27448  noseponlem  27591  nosupbnd1lem3  27637  nosupbnd1lem4  27638  nosupbnd1lem5  27639  nosupbnd2lem1  27642  noinfbnd1lem3  27652  noinfbnd1lem4  27653  noinfbnd1lem5  27654  noetainflem4  27667  scutbdaybnd2lim  27744  tgbtwnne  28288  tgbtwndiff  28304  tgbtwnconn1lem3  28372  legov3  28396  legso  28397  ncolne1  28423  tglineneq  28442  tglowdim2ln  28449  mirne  28465  miriso  28468  mirhl  28477  mirbtwnhl  28478  symquadlem  28487  krippenlem  28488  midexlem  28490  ragflat3  28504  ragperp  28515  footexALT  28516  footexlem2  28518  colperpexlem2  28529  colperpexlem3  28530  mideulem2  28532  oppne3  28541  outpasch  28553  hlpasch  28554  lmieu  28582  lmicom  28586  axlowdim1  28764  wlkp1lem5  29485  wlkp1lem6  29486  eulerpathpr  30044  nmcfnlbi  31856  strlem1  32054  unidifsnne  32326  fsuppcurry1  32502  fsuppcurry2  32503  divnumden2  32576  xrge0npcan  32745  tocyccntz  32860  fracfld  32989  ornglmullt  33017  orngrmullt  33018  pidlnz  33082  drngidl  33144  drngidlhash  33145  rhmpreimaprmidl  33162  qsidomlem1  33163  qsnzr  33166  mxidlirredi  33179  mxidlirred  33180  ssmxidl  33182  krull  33186  qsdrng  33203  zarclsint  33468  zarclssn  33469  xrge0iifhom  33533  qqhf  33582  qqhre  33616  esumrnmpt2  33682  carsgclctunlem2  33934  ballotlemi1  34117  ballotlemii  34118  ballotlemfrcn0  34144  plymulx0  34174  signswn0  34187  signswch  34188  itgexpif  34233  repr0  34238  tgoldbachgtda  34288  pconnconn  34836  unbdqndv2lem2  35980  knoppndvlem13  35994  sucneqond  36839  finxpreclem2  36864  finxp1o  36866  maxidln0  37513  hdmapip0  41383  fldhmf1  41556  hashscontpow1  41587  aks6d1c6lem4  41640  aks6d1c7lem1  41647  metakunt28  41675  metakunt30  41677  remul01  41953  3cubeslem4  42100  3cubes  42101  pellexlem6  42245  nlimsuc  42862  scotteld  43674  mnuprdlem2  43701  inaex  43725  n0p  44398  disjrnmpt2  44552  dstregt0  44654  upbdrech2  44681  xrlexaddrp  44725  infleinflem2  44744  xrralrecnnge  44763  supminfxr2  44842  absimnre  44850  xrpnf  44859  ressioosup  44931  ressiooinf  44933  fmul01lt1lem1  44963  limcperiod  45007  climxrrelem  45128  sinaover2ne0  45247  fperdvper  45298  dvdivbd  45302  itgioocnicc  45356  stirlinglem5  45457  dirker2re  45471  dirkerdenne0  45472  dirkerper  45475  dirkertrigeqlem3  45479  dirkertrigeq  45480  dirkercncflem1  45482  dirkercncflem2  45483  dirkercncflem4  45485  fourierdlem24  45510  fourierdlem25  45511  fourierdlem40  45526  fourierdlem41  45527  fourierdlem42  45528  fourierdlem44  45530  fourierdlem48  45533  fourierdlem49  45534  fourierdlem57  45542  fourierdlem58  45543  fourierdlem59  45544  fourierdlem66  45551  fourierdlem68  45553  fourierdlem74  45559  fourierdlem75  45560  fourierdlem78  45563  fourierdlem80  45565  fourierdlem81  45566  fourierdlem109  45594  elaa2lem  45612  etransclem9  45622  etransclem35  45648  etransclem38  45651  sge0tsms  45759  sge0cl  45760  sge0fodjrnlem  45795  meadjun  45841  meadjiunlem  45844  hoicvr  45927  hoidmvlelem2  45975  hoiqssbllem3  46003  sigardiv  46240  sigarcol  46243  sharhght  46244  prmdvdsfmtnof1lem2  46916  difmodm1lt  47586  fullthinc  48043