Theorem neqned 2964

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

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

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 2958

This theorem is used by:  neqne  2965  necon3bi  2983  necon2ai  2986  necon3i  2989  mteqand  3048  nelne1  3054  nelne2  3055  ne0i  4293  rexn0  4456  nelpr2  4618  nelpr1  4619  otsndisj  5501  rnmptn0  6244  enpr2d  9043  sdomdif  9111  2pwne  9119  mapdom2  9134  dif1enlem  9142  infn0  9260  scotteld  9874  canthp1lem2  10644  nnneneg  12277  flltnz  13851  hashpss  14453  wrdlen2i  14986  s3sndisj  15011  isprm2  16746  isprm5  16772  nnoddn2prmb  16879  chnind  18683  chnccat  18688  hashfinmndnn  18815  sgrp2nmndlem5  18997  fincygsubgodd  20190  prmgrpsimpgd  20192  ornglmullt  20983  orngrmullt  20984  pidlnz  21385  drngidl  21396  rhmpreimaprmidl  21490  qsidomlem1  21491  qsnzr  21494  psdmul  22340  alexsub  24213  ioorf  25743  dvmptdiv  26144  plyn0mulidp  26453  dvtaylp  26544  cos02pilt1  26702  logccne0  26754  isosctrlem1  26994  isosctrlem2  26995  chordthmlem  27008  efrlim  27145  lgsfcl2  27478  lgscllem  27479  lgsval2lem  27482  2sqn0  27609  2sqmod  27611  dchrisumn0  27696  noseponlem  27839  nosupbnd1lem3  27885  nosupbnd1lem4  27886  nosupbnd1lem5  27887  nosupbnd2lem1  27890  noinfbnd1lem3  27900  noinfbnd1lem4  27901  noinfbnd1lem5  27902  noetainflem4  27915  cutbdaybnd2lim  28001  bdayfinbndlem1  28671  z12bdaylem1  28674  tgbtwnne  28770  tgbtwndiff  28786  tgbtwnconn1lem3  28854  legov3  28878  legso  28879  ncolne1  28909  tglineneq  28929  tglowdim2ln  28936  mirne  28955  miriso  28958  mirhl  28967  mirbtwnhl  28968  symquadlem  28977  krippenlem  28978  midexlem  28980  symquadprlnglem  28981  ragflat3  28997  ragperp  29008  footexALT  29009  footexlem2  29011  colperpexlem2  29023  colperpexlem3  29024  mideulem2  29026  oppne3  29035  outpasch  29048  hlpasch  29049  plngrotlem1  29080  lmieu  29104  lmicom  29108  prlngmolem1  29213  prlngmo2  29217  prlngplngtr  29220  prlnginn0  29221  prlngmid2  29222  symquadprlng  29223  quadcgrprlng  29227  axlowdim1  29320  wlkp1lem5  30036  wlkp1lem6  30037  eulerpathpr  30602  nmcfnlbi  32415  strlem1  32613  unidifsnne  32893  fsuppcurry1  33080  fsuppcurry2  33081  divnumden2  33171  xrge0npcan  33349  tocyccntz  33473  elrgspnlem4  33574  fracfld  33638  drngidlhash  33750  mxidlirredi  33763  mxidlirred  33764  ssmxidl  33766  krull  33770  krullndrng  33772  qsdrng  33788  dflringlem  33793  rprmasso2  33825  rprmirred  33830  pidufd  33842  1arithufdlem3  33845  mplmulmvr  33938  esplyind  33974  vietadeg1  33977  exsslsb  33996  constrextdg2lem  34147  constrext2chnlem  34149  2sqr3nconstr  34180  cos9thpinconstrlem2  34189  zarclsint  34271  zarclssn  34272  xrge0iifhom  34336  qqhf  34385  qqhre  34419  esumrnmpt2  34467  carsgclctunlem2  34718  ballotlemi1  34902  ballotlemii  34903  ballotlemfrcn0  34929  signswn0  34956  signswch  34957  itgexpif  35002  repr0  35007  tgoldbachgtda  35057  morleylemrneab  35067  noinfepfnregs  35553  pconnconn  35731  unbdqndv2lem2  37127  knoppndvlem13  37141  qdiff  37999  sucneqond  38039  finxpreclem2  38064  finxp1o  38066  maxidln0  38724  hdmapip0  42717  fldhmf1  42885  hashscontpow1  42916  aks6d1c6lem4  42968  aks6d1c7lem1  42975  remul01  43196  3cubeslem4  43448  3cubes  43449  pellexlem6  43589  nlimsuc  44195  mnuprdlem2  45011  inaex  45035  n0p  45793  disjrnmpt2  45934  dstregt0  46029  upbdrech2  46055  xrlexaddrp  46096  infleinflem2  46114  xrralrecnnge  46133  supminfxr2  46211  absimnre  46218  xrpnf  46227  ressioosup  46299  ressiooinf  46301  fmul01lt1lem1  46328  limcperiod  46372  climxrrelem  46491  sinaover2ne0  46610  fperdvper  46661  dvdivbd  46665  itgioocnicc  46719  stirlinglem5  46820  dirker2re  46834  dirkerdenne0  46835  dirkerper  46838  dirkertrigeqlem3  46842  dirkertrigeq  46843  dirkercncflem1  46845  dirkercncflem2  46846  dirkercncflem4  46848  fourierdlem24  46873  fourierdlem25  46874  fourierdlem40  46889  fourierdlem41  46890  fourierdlem42  46891  fourierdlem44  46893  fourierdlem48  46896  fourierdlem49  46897  fourierdlem57  46905  fourierdlem58  46906  fourierdlem59  46907  fourierdlem66  46914  fourierdlem68  46916  fourierdlem74  46922  fourierdlem75  46923  fourierdlem78  46926  fourierdlem80  46928  fourierdlem81  46929  fourierdlem109  46957  elaa2lem  46975  etransclem9  46985  etransclem35  47011  etransclem38  47014  sge0tsms  47122  sge0cl  47123  sge0fodjrnlem  47158  meadjun  47204  meadjiunlem  47207  hoicvr  47290  hoidmvlelem2  47338  hoiqssbllem3  47366  sigardiv  47603  sigarcol  47606  sharhght  47607  chnsubseq  47624  difltmodne  48113  minusmodnep2tmod  48124  modm1p1ne  48141  prmdvdsfmtnof1lem2  48365  gpg3kgrtriexlem5  48880  fucofvalne  50131  fullthinc  50256  euendfunc2  50333