Theorem neqned 2962

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

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   = wceq 1570   ≠ wne 2955

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-ne 2956

This theorem is used by:  neqne  2963  necon3bi  2981  necon2ai  2984  necon3i  2987  mteqand  3046  nelne1  3052  nelne2  3053  ne0i  4286  rexn0  4451  nelpr2  4613  nelpr1  4614  otsndisj  5488  rnmptn0  6234  enpr2d  9054  sdomdif  9122  2pwne  9130  mapdom2  9145  dif1enlem  9153  infn0  9272  scotteld  9918  canthp1lem2  10709  nnneneg  12342  flltnz  13919  hashpss  14521  wrdlen2i  15060  s3sndisj  15087  isprm2  16819  isprm5  16845  nnoddn2prmb  16952  chnind  18756  chnccat  18761  hashfinmndnn  18902  sgrp2nmndlem5  19089  fincygsubgodd  20289  prmgrpsimpgd  20291  ornglmullt  21087  orngrmullt  21088  pidlnz  21489  drngidl  21500  rhmpreimaprmidl  21596  qsidomlem1  21597  qsnzr  21600  psdmul  22448  alexsub  24325  ioorf  25855  dvmptdiv  26255  plyn0mulidp  26565  dvtaylp  26660  cos02pilt1  26817  logccne0  26869  isosctrlem1  27109  isosctrlem2  27110  chordthmlem  27123  efrlim  27260  lgsfcl2  27593  lgscllem  27594  lgsval2lem  27597  2sqn0  27724  2sqmod  27726  dchrisumn0  27811  noseponlem  27954  nosupbnd1lem3  28000  nosupbnd1lem4  28001  nosupbnd1lem5  28002  nosupbnd2lem1  28005  noinfbnd1lem3  28015  noinfbnd1lem4  28016  noinfbnd1lem5  28017  noetainflem4  28030  cutbdaybnd2lim  28116  bdayfinbndlem1  28786  z12bdaylem1  28789  tgbtwnne  28886  tgbtwndiff  28902  tgbtwnconn1lem3  28970  legov3  28994  legso  28995  ncolne1  29026  tglineneq  29046  tglowdim2ln  29053  mirne  29072  miriso  29075  mirhl  29084  mirbtwnhl  29085  symquadlem  29094  krippenlem  29095  midexlem  29097  symquadprlnglem  29098  ragflat3  29114  ragperp  29125  footexALT  29126  footexlem2  29128  colperpexlem2  29140  colperpexlem3  29141  mideulem2  29143  oppne3  29152  outpasch  29166  hlpasch  29167  plngrotlem1  29198  lmieu  29222  lmicom  29226  tgaaddcpbllem1  29282  tgaaddcpbllem2  29283  angmgmaddeu1  29312  angmgmaddov2lem  29320  prlngmolem1  29363  prlngmo2  29367  prlngplngtr  29370  prlnginn0  29371  prlngmid2  29372  symquadprlng  29373  quadcgrprlng  29377  axlowdim1  29470  wlkp1lem5  30189  wlkp1lem6  30190  eulerpathpr  30774  nmcfnlbi  32587  strlem1  32785  unidifsnne  33065  fsuppcurry1  33249  fsuppcurry2  33250  divnumden2  33340  xrge0npcan  33514  tocyccntz  33638  elrgspnlem4  33739  fracfld  33803  drngidlhash  33916  mxidlirredi  33929  mxidlirred  33930  ssmxidl  33932  krull  33936  krullndrng  33938  qsdrng  33954  dflringlem  33959  rprmasso2  33991  rprmirred  33996  pidufd  34008  1arithufdlem3  34011  mplmulmvr  34104  esplyind  34140  vietadeg1  34143  exsslsb  34162  constrextdg2lem  34313  constrext2chnlem  34315  2sqr3nconstr  34346  cos9thpinconstrlem2  34355  zarclsint  34437  zarclssn  34438  xrge0iifhom  34502  qqhf  34551  qqhre  34585  esumrnmpt2  34633  carsgclctunlem2  34885  ballotlemi1  35069  ballotlemii  35070  ballotlemfrcn0  35096  signswn0  35123  signswch  35124  itgexpif  35169  repr0  35174  tgoldbachgtda  35224  morleylemrneab  35234  noinfepfnregs  35725  pconnconn  35917  unbdqndv2lem2  37298  knoppndvlem13  37312  qdiff  38168  sucneqond  38208  finxpreclem2  38233  finxp1o  38235  maxidln0  38899  hdmapip0  42892  fldhmf1  43060  hashscontpow1  43091  aks6d1c6lem4  43143  aks6d1c7lem1  43150  remul01  43386  3cubeslem4  43638  3cubes  43639  pellexlem6  43779  nlimsuc  44385  mnuprdlem2  45201  inaex  45225  n0p  45983  disjrnmpt2  46124  dstregt0  46219  upbdrech2  46245  xrlexaddrp  46286  infleinflem2  46304  xrralrecnnge  46323  supminfxr2  46401  absimnre  46408  xrpnf  46417  ressioosup  46489  ressiooinf  46491  fmul01lt1lem1  46518  limcperiod  46562  climxrrelem  46681  sinaover2ne0  46800  fperdvper  46851  dvdivbd  46855  itgioocnicc  46909  stirlinglem5  47010  dirker2re  47024  dirkerdenne0  47025  dirkerper  47028  dirkertrigeqlem3  47032  dirkertrigeq  47033  dirkercncflem1  47035  dirkercncflem2  47036  dirkercncflem4  47038  fourierdlem24  47063  fourierdlem25  47064  fourierdlem40  47079  fourierdlem41  47080  fourierdlem42  47081  fourierdlem44  47083  fourierdlem48  47086  fourierdlem49  47087  fourierdlem57  47095  fourierdlem58  47096  fourierdlem59  47097  fourierdlem66  47104  fourierdlem68  47106  fourierdlem74  47112  fourierdlem75  47113  fourierdlem78  47116  fourierdlem80  47118  fourierdlem81  47119  fourierdlem109  47147  elaa2lem  47165  etransclem9  47175  etransclem35  47201  etransclem38  47204  sge0tsms  47312  sge0cl  47313  sge0fodjrnlem  47348  meadjun  47394  meadjiunlem  47397  hoicvr  47480  hoidmvlelem2  47528  hoiqssbllem3  47556  sigardiv  47793  sigarcol  47796  sharhght  47797  difltmodne  48340  minusmodnep2tmod  48351  modm1p1ne  48368  prmdvdsfmtnof1lem2  48592  gpg3kgrtriexlem5  49107  fucofvalne  50355  fullthinc  50480  euendfunc2  50557