Theorem neqned 2949

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

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1539   ≠ wne 2942

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 2943

This theorem is referenced by:  neqne  2950  necon3bi  2969  necon2ai  2972  necon3i  2975  nelne1  3040  nelne2  3041  mteqand  3047  ne0i  4265  rexn0  4438  nelpr2  4585  nelpr1  4586  otsndisj  5427  rnmptn0  6136  enpr2d  8792  sdomdif  8861  2pwne  8869  mapdom2  8884  dif1enlem  8905  canthp1lem2  10340  nnneneg  11938  flltnz  13459  wrdlen2i  14583  s3sndisj  14606  isprm2  16315  isprm5  16340  nnoddn2prmb  16442  hashfinmndnn  18317  sgrp2nmndlem5  18483  fincygsubgodd  19630  prmgrpsimpgd  19632  alexsub  23104  ioorf  24642  dvmptdiv  25043  dvtaylp  25434  cos02pilt1  25587  logccne0  25639  isosctrlem1  25873  isosctrlem2  25874  chordthmlem  25887  efrlim  26024  lgsfcl2  26356  lgscllem  26357  lgsval2lem  26360  2sqn0  26487  2sqmod  26489  dchrisumn0  26574  tgbtwnne  26755  tgbtwndiff  26771  tgbtwnconn1lem3  26839  legov3  26863  legso  26864  ncolne1  26890  tglineneq  26909  tglowdim2ln  26916  mirne  26932  miriso  26935  mirhl  26944  mirbtwnhl  26945  symquadlem  26954  krippenlem  26955  midexlem  26957  ragflat3  26971  ragperp  26982  footexALT  26983  footexlem2  26985  colperpexlem2  26996  colperpexlem3  26997  mideulem2  26999  oppne3  27008  outpasch  27020  hlpasch  27021  lmieu  27049  lmicom  27053  axlowdim1  27230  wlkp1lem5  27947  wlkp1lem6  27948  eulerpathpr  28505  nmcfnlbi  30315  strlem1  30513  unidifsnne  30785  fsuppcurry1  30962  fsuppcurry2  30963  divnumden2  31034  xrge0npcan  31205  tocyccntz  31313  ornglmullt  31408  orngrmullt  31409  pidlnz  31473  rhmpreimaprmidl  31529  qsidomlem1  31530  ssmxidl  31544  krull  31545  zarclsint  31724  zarclssn  31725  xrge0iifhom  31789  qqhf  31836  qqhre  31870  esumrnmpt2  31936  carsgclctunlem2  32186  ballotlemi1  32369  ballotlemii  32370  ballotlemfrcn0  32396  plymulx0  32426  signswn0  32439  signswch  32440  itgexpif  32486  repr0  32491  tgoldbachgtda  32541  pconnconn  33093  noseponlem  33794  nosupbnd1lem3  33840  nosupbnd1lem4  33841  nosupbnd1lem5  33842  nosupbnd2lem1  33845  noinfbnd1lem3  33855  noinfbnd1lem4  33856  noinfbnd1lem5  33857  noetainflem4  33870  scutbdaybnd2lim  33938  unbdqndv2lem2  34617  knoppndvlem13  34631  sucneqond  35463  finxpreclem2  35488  finxp1o  35490  maxidln0  36130  hdmapip0  39856  metakunt28  40080  metakunt30  40082  remul01  40311  3cubeslem4  40427  3cubes  40428  pellexlem6  40572  scotteld  41753  mnuprdlem2  41780  inaex  41804  n0p  42480  disjrnmpt2  42615  dstregt0  42709  upbdrech2  42737  xrlexaddrp  42781  infleinflem2  42800  xrralrecnnge  42820  supminfxr2  42899  absimnre  42907  xrpnf  42916  ressioosup  42983  ressiooinf  42985  fmul01lt1lem1  43015  limcperiod  43059  climxrrelem  43180  sinaover2ne0  43299  fperdvper  43350  dvdivbd  43354  itgioocnicc  43408  stirlinglem5  43509  dirker2re  43523  dirkerdenne0  43524  dirkerper  43527  dirkertrigeqlem3  43531  dirkertrigeq  43532  dirkercncflem1  43534  dirkercncflem2  43535  dirkercncflem4  43537  fourierdlem24  43562  fourierdlem25  43563  fourierdlem40  43578  fourierdlem41  43579  fourierdlem42  43580  fourierdlem44  43582  fourierdlem48  43585  fourierdlem49  43586  fourierdlem57  43594  fourierdlem58  43595  fourierdlem59  43596  fourierdlem66  43603  fourierdlem68  43605  fourierdlem74  43611  fourierdlem75  43612  fourierdlem78  43615  fourierdlem80  43617  fourierdlem81  43618  fourierdlem109  43646  elaa2lem  43664  etransclem9  43674  etransclem35  43700  etransclem38  43703  sge0tsms  43808  sge0cl  43809  sge0fodjrnlem  43844  meadjun  43890  meadjiunlem  43893  hoicvr  43976  hoidmvlelem2  44024  hoiqssbllem3  44052  sigardiv  44264  sigarcol  44267  sharhght  44268  prmdvdsfmtnof1lem2  44925  difmodm1lt  45756  fullthinc  46215