Theorem neqned 2963

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

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1568   ≠ wne 2956

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 210  df-ne 2957

This theorem is referenced by:  neqne  2964  necon3bi  2982  necon2ai  2985  necon3i  2988  mteqand  3047  nelne1  3053  nelne2  3054  ne0i  4293  rexn0  4456  nelpr2  4618  nelpr1  4619  otsndisj  5502  rnmptn0  6245  enpr2d  9044  sdomdif  9112  2pwne  9120  mapdom2  9135  dif1enlem  9143  infn0  9261  scotteld  9871  canthp1lem2  10637  nnneneg  12270  flltnz  13843  hashpss  14445  wrdlen2i  14978  s3sndisj  15003  isprm2  16739  isprm5  16765  nnoddn2prmb  16872  chnind  18676  chnccat  18681  hashfinmndnn  18808  sgrp2nmndlem5  18990  fincygsubgodd  20183  prmgrpsimpgd  20185  ornglmullt  20951  orngrmullt  20952  pidlnz  21353  drngidl  21364  rhmpreimaprmidl  21458  qsidomlem1  21459  qsnzr  21462  psdmul  22308  alexsub  24181  ioorf  25711  dvmptdiv  26112  plyn0mulidp  26421  dvtaylp  26509  cos02pilt1  26667  logccne0  26719  isosctrlem1  26959  isosctrlem2  26960  chordthmlem  26973  efrlim  27110  lgsfcl2  27443  lgscllem  27444  lgsval2lem  27447  2sqn0  27574  2sqmod  27576  dchrisumn0  27661  noseponlem  27804  nosupbnd1lem3  27850  nosupbnd1lem4  27851  nosupbnd1lem5  27852  nosupbnd2lem1  27855  noinfbnd1lem3  27865  noinfbnd1lem4  27866  noinfbnd1lem5  27867  noetainflem4  27880  cutbdaybnd2lim  27966  bdayfinbndlem1  28636  z12bdaylem1  28639  tgbtwnne  28735  tgbtwndiff  28751  tgbtwnconn1lem3  28819  legov3  28843  legso  28844  ncolne1  28874  tglineneq  28894  tglowdim2ln  28901  mirne  28920  miriso  28923  mirhl  28932  mirbtwnhl  28933  symquadlem  28942  krippenlem  28943  midexlem  28945  ragflat3  28961  ragperp  28972  footexALT  28973  footexlem2  28975  colperpexlem2  28987  colperpexlem3  28988  mideulem2  28990  oppne3  28999  outpasch  29012  hlpasch  29013  plngrotlem1  29043  lmieu  29067  lmicom  29071  prlngmolem1  29175  prlngmo2  29179  prlngplngtr  29181  prlnginn0  29182  prlngmid2  29183  axlowdim1  29275  wlkp1lem5  29991  wlkp1lem6  29992  eulerpathpr  30557  nmcfnlbi  32370  strlem1  32568  unidifsnne  32848  fsuppcurry1  33035  fsuppcurry2  33036  divnumden2  33126  xrge0npcan  33306  tocyccntz  33430  elrgspnlem4  33531  fracfld  33595  drngidlhash  33707  mxidlirredi  33720  mxidlirred  33721  ssmxidl  33723  krull  33727  krullndrng  33729  qsdrng  33745  dflringlem  33750  rprmasso2  33782  rprmirred  33787  pidufd  33799  1arithufdlem3  33802  mplmulmvr  33895  esplyind  33931  vietadeg1  33934  exsslsb  33953  constrextdg2lem  34104  constrext2chnlem  34106  2sqr3nconstr  34137  cos9thpinconstrlem2  34146  zarclsint  34228  zarclssn  34229  xrge0iifhom  34293  qqhf  34342  qqhre  34376  esumrnmpt2  34424  carsgclctunlem2  34675  ballotlemi1  34859  ballotlemii  34860  ballotlemfrcn0  34886  signswn0  34913  signswch  34914  itgexpif  34959  repr0  34964  tgoldbachgtda  35014  morleylemrneab  35024  noinfepfnregs  35499  pconnconn  35677  unbdqndv2lem2  37043  knoppndvlem13  37057  qdiff  37915  sucneqond  37955  finxpreclem2  37980  finxp1o  37982  maxidln0  38640  hdmapip0  42635  fldhmf1  42803  hashscontpow1  42834  aks6d1c6lem4  42886  aks6d1c7lem1  42893  remul01  43114  3cubeslem4  43368  3cubes  43369  pellexlem6  43509  nlimsuc  44115  mnuprdlem2  44931  inaex  44955  n0p  45713  disjrnmpt2  45854  dstregt0  45949  upbdrech2  45975  xrlexaddrp  46016  infleinflem2  46034  xrralrecnnge  46053  supminfxr2  46131  absimnre  46138  xrpnf  46147  ressioosup  46219  ressiooinf  46221  fmul01lt1lem1  46248  limcperiod  46292  climxrrelem  46411  sinaover2ne0  46530  fperdvper  46581  dvdivbd  46585  itgioocnicc  46639  stirlinglem5  46740  dirker2re  46754  dirkerdenne0  46755  dirkerper  46758  dirkertrigeqlem3  46762  dirkertrigeq  46763  dirkercncflem1  46765  dirkercncflem2  46766  dirkercncflem4  46768  fourierdlem24  46793  fourierdlem25  46794  fourierdlem40  46809  fourierdlem41  46810  fourierdlem42  46811  fourierdlem44  46813  fourierdlem48  46816  fourierdlem49  46817  fourierdlem57  46825  fourierdlem58  46826  fourierdlem59  46827  fourierdlem66  46834  fourierdlem68  46836  fourierdlem74  46842  fourierdlem75  46843  fourierdlem78  46846  fourierdlem80  46848  fourierdlem81  46849  fourierdlem109  46877  elaa2lem  46895  etransclem9  46905  etransclem35  46931  etransclem38  46934  sge0tsms  47042  sge0cl  47043  sge0fodjrnlem  47078  meadjun  47124  meadjiunlem  47127  hoicvr  47210  hoidmvlelem2  47258  hoiqssbllem3  47286  sigardiv  47523  sigarcol  47526  sharhght  47527  chnsubseq  47544  difltmodne  48030  minusmodnep2tmod  48041  modm1p1ne  48058  prmdvdsfmtnof1lem2  48282  gpg3kgrtriexlem5  48797  fucofvalne  50048  fullthinc  50173  euendfunc2  50250